Publications - Current Year

“Formal Verification of Logical Calculi and Simulations in Isabelle/HOL,” Universität des Saarlandes, Saarbrücken, 2025.

@phdthesis{ThesisPhDDesharnais2025,
TITLE = {Formal Verification of Logical Calculi and Simulations in {Isabelle/HOL}},
AUTHOR = {Desharnais, Martin},
LANGUAGE = {eng},
URL = {urn:nbn:de:bsz:291--ds-450437},
DOI = {10.22028/D291-45043},
SCHOOL = {Universit{\"a}t des Saarlandes},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2025},
MARGINALMARK = {$\bullet$},
DATE = {2025},
}

%0 Thesis
%A Desharnais, Martin
%Y Weidenbach, Christoph
%A referee: Bromberger, Martin
%A referee: Tourret, Sophie
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Formal Verification of Logical Calculi and Simulations in Isabelle/HOL : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0011-77DB-1
%R 10.22028/D291-45043
%U urn:nbn:de:bsz:291--ds-450437
%F OTHER: hdl:20.500.11880/39960
%I Universität des Saarlandes
%C Saarbrücken
%D 2025
%P XII, 155 p.
%V phd
%9 phd
%U http://dx.doi.org/10.22028/D291-45043

“SCL(EQ): Simple Clause Learning in First-order Logic with Equality,” Universität des Saarlandes, Saarbrücken, 2025.

@phdthesis{ThesisPhDLeidinger2025,
TITLE = {{SCL(EQ)}: {S}imple Clause Learning in First-order Logic with Equality},
AUTHOR = {Leidinger, Hendrik},
LANGUAGE = {eng},
URL = {urn:nbn:de:bsz:291--ds-455521},
DOI = {10.22028/D291-45552},
SCHOOL = {Universit{\"a}t des Saarlandes},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2025},
MARGINALMARK = {$\bullet$},
DATE = {2025},
}

%0 Thesis
%A Leidinger, Hendrik
%Y Weidenbach, Christoph
%A referee: Fontaine, Pascal
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T SCL(EQ): Simple Clause Learning in First-order Logic with Equality : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0011-7985-F
%R 10.22028/D291-45552
%U urn:nbn:de:bsz:291--ds-455521
%F OTHER: hdl:20.500.11880/40100
%I Universität des Saarlandes
%C Saarbrücken
%D 2025
%P X, 102 p.
%V phd
%9 phd
%U http://dx.doi.org/10.22028/D291-45552

“On Enumerating Short Projected Models,” Discrete Applied Mathematics, vol. 361, 2025.

@article{Moehle25,
TITLE = {On Enumerating Short Projected Models},
AUTHOR = {M{\"o}hle, Sibylle and Sebastiani, Roberto and Biere, Armin},
LANGUAGE = {eng},
ISSN = {0166-218X},
DOI = {10.1016/j.dam.2024.10.021},
PUBLISHER = {Elsevier},
ADDRESS = {Amsterdam},
YEAR = {2025},
MARGINALMARK = {$\bullet$},
DATE = {2025},
JOURNAL = {Discrete Applied Mathematics},
VOLUME = {361},
PAGES = {412--439},
}

%0 Journal Article
%A Möhle, Sibylle
%A Sebastiani, Roberto
%A Biere, Armin
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
%T On Enumerating Short Projected Models : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-80F4-9
%R 10.1016/j.dam.2024.10.021
%7 2024-11-12
%D 2025
%J Discrete Applied Mathematics
%V 361
%& 412
%P 412 - 439
%I Elsevier
%C Amsterdam
%@ false