Current Year
Barbosa, H., Blanchette, J. C., & Fontaine, P. (2020). Scalable Fine-Grained Proofs for Formula Processing. Journal of Automated Reasoning, 64(3). doi:10.1007/s10817-018-09502-y
Export
BibTeX
@article{Barbosa2020,
TITLE = {Scalable Fine-Grained Proofs for Formula Processing},
AUTHOR = {Barbosa, Haniel and Blanchette, Jasmin Christian and Fontaine, Pascal},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-018-09502-y},
PUBLISHER = {D. Reidel Pub. Co.},
ADDRESS = {Dordrecht, Holland},
YEAR = {2020},
DATE = {2020},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {64},
NUMBER = {3},
PAGES = {485--510},
}
Endnote
%0 Journal Article
%A Barbosa, Haniel
%A Blanchette, Jasmin Christian
%A Fontaine, Pascal
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Scalable Fine-Grained Proofs for Formula Processing :
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-908A-B
%R 10.1007/s10817-018-09502-y
%7 2020
%D 2020
%J Journal of Automated Reasoning
%V 64
%N 3
%& 485
%P 485 - 510
%I D. Reidel Pub. Co.
%C Dordrecht, Holland
%@ false
Biere, A., Tinelli, C., & Weidenbach, C. (2020). Preface to the Special Issue on Automated Reasoning Systems. Journal of Automated Reasoning, 64(3). doi:10.1007/s10817-019-09531-1
Export
BibTeX
@article{Biere2020,
TITLE = {Preface to the Special Issue on Automated Reasoning Systems},
AUTHOR = {Biere, Armin and Tinelli, Cesare and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-019-09531-1},
PUBLISHER = {D. Reidel Pub. Co.},
ADDRESS = {Dordrecht, Holland},
YEAR = {2020},
DATE = {2020},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {64},
NUMBER = {3},
PAGES = {361--362},
}
Endnote
%0 Journal Article
%A Biere, Armin
%A Tinelli, Cesare
%A Weidenbach, Christoph
%+ External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Preface to the Special Issue on Automated Reasoning Systems :
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-908E-7
%R 10.1007/s10817-019-09531-1
%7 2020
%D 2020
%J Journal of Automated Reasoning
%V 64
%N 3
%& 361
%P 361 - 362
%I D. Reidel Pub. Co.
%C Dordrecht, Holland
%@ false
Bradford, R., Davenport, J. H., England, M., Errami, H., Gerdt, V., Grigoriev, D., … Weber, A. (2020). Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks. Journal of Symbolic Computation, 98. doi:10.1016/j.jsc.2019.07.008
Export
BibTeX
@article{BradfordDavenport:19a,
TITLE = {Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks},
AUTHOR = {Bradford, Russell and Davenport, James H. and England, Matthew and Errami, Hassan and Gerdt, Vladimir and Grigoriev, Dima and Hoyt, Charles and Ko{\v s}ta, Marek and Radulescu, Ovidiu and Sturm, Thomas and Weber, Andreas},
LANGUAGE = {eng},
ISSN = {0747-7171},
DOI = {10.1016/j.jsc.2019.07.008},
PUBLISHER = {Academic Press},
ADDRESS = {London},
YEAR = {2020},
DATE = {2020},
JOURNAL = {Journal of Symbolic Computation},
VOLUME = {98},
PAGES = {84--119},
}
Endnote
%0 Journal Article
%A Bradford, Russell
%A Davenport, James H.
%A England, Matthew
%A Errami, Hassan
%A Gerdt, Vladimir
%A Grigoriev, Dima
%A Hoyt, Charles
%A Košta, Marek
%A Radulescu, Ovidiu
%A Sturm, Thomas
%A Weber, Andreas
%+ External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks :
%G eng
%U http://hdl.handle.net/21.11116/0000-0002-F04B-B
%R 10.1016/j.jsc.2019.07.008
%7 2020
%D 2020
%J Journal of Symbolic Computation
%V 98
%& 84
%P 84 - 119
%I Academic Press
%C London
%@ false
Bromberger, M., Sturm, T., & Weidenbach, C. (2020). A Complete and Terminating Approach to Linear Integer Solving. Journal of Symbolic Computation, 100. doi:10.1016/j.jsc.2019.07.021
Export
BibTeX
@article{Bromberger2020,
TITLE = {A Complete and Terminating Approach to Linear Integer Solving},
AUTHOR = {Bromberger, Martin and Sturm, Thomas and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0747-7171},
DOI = {10.1016/j.jsc.2019.07.021},
PUBLISHER = {Academic Press},
ADDRESS = {London},
YEAR = {2020},
DATE = {2020},
JOURNAL = {Journal of Symbolic Computation},
VOLUME = {100},
PAGES = {102--136},
}
Endnote
%0 Journal Article
%A Bromberger, Martin
%A Sturm, Thomas
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Complete and Terminating Approach to Linear Integer Solving :
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-99CD-7
%R 10.1016/j.jsc.2019.07.021
%7 2019
%D 2020
%J Journal of Symbolic Computation
%V 100
%& 102
%P 102 - 136
%I Academic Press
%C London
%@ false
Davenport, J. H., England, M., Griggio, A., Sturm, T., & Tinelli, C. (2020). Symbolic Computation and Satisfiability Checking. Journal of Symbolic Computation, 100. doi:10.1016/j.jsc.2019.07.017
Export
BibTeX
@article{Davenport2020,
TITLE = {Symbolic Computation and Satisfiability Checking},
AUTHOR = {Davenport, James H. and England, Matthew and Griggio, Alberto and Sturm, Thomas and Tinelli, Cesare},
LANGUAGE = {eng},
ISSN = {0747-7171},
DOI = {10.1016/j.jsc.2019.07.017},
PUBLISHER = {Academic Press},
ADDRESS = {London},
YEAR = {2020},
DATE = {2020},
JOURNAL = {Journal of Symbolic Computation},
VOLUME = {100},
PAGES = {1--10},
}
Endnote
%0 Journal Article
%A Davenport, James H.
%A England, Matthew
%A Griggio, Alberto
%A Sturm, Thomas
%A Tinelli, Cesare
%+ External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Symbolic Computation and Satisfiability Checking : Editorial
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-99CF-5
%R 10.1016/j.jsc.2019.07.017
%7 2020
%D 2020
%J Journal of Symbolic Computation
%V 100
%& 1
%P 1 - 10
%I Academic Press
%C London
%@ false
Fleury, M. (2020). Formalization of logical calculi in Isabelle/HOL. Universität des Saarlandes, Saarbrücken.
Abstract
I develop a formal framework for propositional satifisfiability with the conflict-driven clause learning (CDCL) procedure using the Isabelle/HOL proof assistant. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland procedure. The most noteworthy aspects of my work are the inclusion of rules for forget and restart and the refinement approach. I use the formalization to develop three extensions: First, an incremental solving extension of CDCL. Second, I verify an optimizing CDCL (OCDCL): Given a cost function on literals, OCDCL derives an optimal model with minimum cost. Finally, I work on model covering. Thanks to the CDCL framework I can reuse, these extensions are easier to develop. Through a chain of refinements, I connect the abstract CDCL calculus first to a more concrete calculus, then to a SAT solver expressed in a simple functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The imperative version relies on the two-watched-literal data structure and other optimizations found in modern solvers. I used the Isabelle Refinement Framework to automate the most tedious refinement steps. After that, I extend this work with further optimizations like blocking literals and the use of machine words as long as possible, before switching to unbounded integers to keep completeness.
Export
BibTeX
@phdthesis{Fleuryphd2019,
TITLE = {Formalization of logical calculi in Isabelle/{HOL}},
AUTHOR = {Fleury, Mathias},
LANGUAGE = {eng},
DOI = {10.22028/D291-30179},
SCHOOL = {Universit{\"a}t des Saarlandes},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2020},
DATE = {2020},
ABSTRACT = {I develop a formal framework for propositional satifisfiability with the conflict-driven clause learning (CDCL) procedure using the Isabelle/HOL proof assistant. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland procedure. The most noteworthy aspects of my work are the inclusion of rules for forget and restart and the refinement approach. I use the formalization to develop three extensions: First, an incremental solving extension of CDCL. Second, I verify an optimizing CDCL (OCDCL): Given a cost function on literals, OCDCL derives an optimal model with minimum cost. Finally, I work on model covering. Thanks to the CDCL framework I can reuse, these extensions are easier to develop. Through a chain of refinements, I connect the abstract CDCL calculus first to a more concrete calculus, then to a SAT solver expressed in a simple functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The imperative version relies on the two-watched-literal data structure and other optimizations found in modern solvers. I used the Isabelle Refinement Framework to automate the most tedious refinement steps. After that, I extend this work with further optimizations like blocking literals and the use of machine words as long as possible, before switching to unbounded integers to keep completeness.},
}
Endnote
%0 Thesis
%A Fleury, Mathias
%Y Weidenbach, Christoph
%A referee: Biere, Armin
%+ Automation of Logic, MPI for Informatics, Max Planck Society
International Max Planck Research School, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Formalization of logical calculi in Isabelle/HOL :
%G eng
%U http://hdl.handle.net/21.11116/0000-0005-AE07-0
%R 10.22028/D291-30179
%I Universität des Saarlandes
%C Saarbrücken
%D 2020
%P 169 p.
%V phd
%9 phd
%X I develop a formal framework for propositional satifisfiability with the conflict-driven clause learning (CDCL) procedure using the Isabelle/HOL proof assistant. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland procedure. The most noteworthy aspects of my work are the inclusion of rules for forget and restart and the refinement approach. I use the formalization to develop three extensions: First, an incremental solving extension of CDCL. Second, I verify an optimizing CDCL (OCDCL): Given a cost function on literals, OCDCL derives an optimal model with minimum cost. Finally, I work on model covering. Thanks to the CDCL framework I can reuse, these extensions are easier to develop. Through a chain of refinements, I connect the abstract CDCL calculus first to a more concrete calculus, then to a SAT solver expressed in a simple functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The imperative version relies on the two-watched-literal data structure and other optimizations found in modern solvers. I used the Isabelle Refinement Framework to automate the most tedious refinement steps. After that, I extend this work with further optimizations like blocking literals and the use of machine words as long as possible, before switching to unbounded integers to keep completeness.
%U https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28722
Schlichtkrull, A., Blanchette, J. C., Traytel, D., & Waldmann, U. (2020). Formalizing of Bachmair and Ganzinger’s Ordered Resolution Prover. Journal of Automated Reasoning. doi:10.1007/s10817-020-09561-0
Export
BibTeX
@article{Schlichtkrull_JAR2020,
TITLE = {Formalizing of {B}achmair and {G}anzinger's Ordered Resolution Prover},
AUTHOR = {Schlichtkrull, Anders and Blanchette, Jasmin Christian and Traytel, Dmitriy and Waldmann, Uwe},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-020-09561-0},
PUBLISHER = {D. Reidel Pub. Co.},
ADDRESS = {Dordrecht, Holland},
YEAR = {2020},
JOURNAL = {Journal of Automated Reasoning},
}
Endnote
%0 Journal Article
%A Schlichtkrull, Anders
%A Blanchette, Jasmin Christian
%A Traytel, Dmitriy
%A Waldmann, Uwe
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Formalizing of Bachmair and Ganzinger's Ordered Resolution Prover :
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-A2B5-6
%R 10.1007/s10817-020-09561-0
%7 2020
%D 2020
%J Journal of Automated Reasoning
%I D. Reidel Pub. Co.
%C Dordrecht, Holland
%@ false
Teucke, A., & Weidenbach, C. (2020). SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment. Journal of Automated Reasoning, 64(3). doi:10.1007/s10817-020-09546-z
Export
BibTeX
@article{Teucke2020,
TITLE = {{SPASS-AR}: {A} First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment},
AUTHOR = {Teucke, Andreas and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-020-09546-z},
PUBLISHER = {D. Reidel Pub. Co.},
ADDRESS = {Dordrecht, Holland},
YEAR = {2020},
DATE = {2020},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {64},
NUMBER = {3},
PAGES = {611--640},
}
Endnote
%0 Journal Article
%A Teucke, Andreas
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment :
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-9084-1
%R 10.1007/s10817-020-09546-z
%7 2020
%D 2020
%J Journal of Automated Reasoning
%V 64
%N 3
%& 611
%P 611 - 640
%I D. Reidel Pub. Co.
%C Dordrecht, Holland
%@ false
Voigt, M. (2020). Decidable ∃∗∀∗ First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates. Journal of Automated Reasoning. doi:10.1007/s10817-020-09567-8
Export
BibTeX
@article{Voigt2020,
TITLE = {Decidable {\exists }^*{\forall }^* First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates},
AUTHOR = {Voigt, Marco},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-020-09567-8},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2020},
JOURNAL = {Journal of Automated Reasoning},
}
Endnote
%0 Journal Article
%A Voigt, Marco
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T Decidable ∃∗∀∗ First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates :
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-DC7C-8
%R 10.1007/s10817-020-09567-8
%7 2020
%D 2020
%J Journal of Automated Reasoning
%I Springer
%C New York, NY
%@ false