Current Year

Azmy, N., Merz, S., & Weidenbach, C. (2018). A Machine-checked Correctness Proof for Pastry. Science of Computer Programming, 158. doi:10.1016/j.scico.2017.08.003
Export
BibTeX
@article{Azmy2018, TITLE = {A machine-checked correctness proof for {Pastry}}, AUTHOR = {Azmy, Noran and Merz, Stephan and Weidenbach, Christoph}, LANGUAGE = {eng}, ISSN = {0167-6423}, DOI = {10.1016/j.scico.2017.08.003}, PUBLISHER = {Elsevier}, ADDRESS = {Amsterdam}, YEAR = {2018}, DATE = {2018}, JOURNAL = {Science of Computer Programming}, VOLUME = {158}, PAGES = {64--80}, }
Endnote
%0 Journal Article %A Azmy, Noran %A Merz, Stephan %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 Machine-checked Correctness Proof for Pastry : %G eng %U http://hdl.handle.net/21.11116/0000-0001-4F95-F %R 10.1016/j.scico.2017.08.003 %7 2017 %D 2018 %J Science of Computer Programming %V 158 %& 64 %P 64 - 80 %I Elsevier %C Amsterdam %@ false
Blanchette, J. C., Fleury, M., Lammich, P., & Weidenbach, C. (2018). A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. Journal of Automated Reasoning, 61(1-4). doi:10.1007/s10817-018-9455-7
Export
BibTeX
@article{Blanchette2018, TITLE = {A Verified {SAT} Solver Framework with Learn, Forget, Restart, and Incrementality}, AUTHOR = {Blanchette, Jasmin Christian and Fleury, Mathias and Lammich, Peter and Weidenbach, Christoph}, LANGUAGE = {eng}, ISSN = {0168-7433}, DOI = {10.1007/s10817-018-9455-7}, PUBLISHER = {Springer}, ADDRESS = {New York, NY}, YEAR = {2018}, DATE = {2018}, JOURNAL = {Journal of Automated Reasoning}, VOLUME = {61}, NUMBER = {1-4}, PAGES = {333--365}, }
Endnote
%0 Journal Article %A Blanchette, Jasmin Christian %A Fleury, Mathias %A Lammich, Peter %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality : %G eng %U http://hdl.handle.net/21.11116/0000-0001-7ADB-0 %R 10.1007/s10817-018-9455-7 %7 2018 %D 2018 %J Journal of Automated Reasoning %V 61 %N 1-4 %& 333 %P 333 - 365 %I Springer %C New York, NY %@ false
Fleury, M., Blanchette, J. C., & Lammich, P. (2018). A Verified SAT Solver with Watched Literals using Imperative HOL. In CPP’18, 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. Los Angeles, CA, USA: ACM. doi:10.1145/3167080
Export
BibTeX
@inproceedings{FleuryCPP2018, TITLE = {A verified {SAT} solver with watched literals using imperative {HOL}}, AUTHOR = {Fleury, Mathias and Blanchette, Jasmin Christian and Lammich, Peter}, LANGUAGE = {eng}, ISBN = {978-1-4503-5586-5}, DOI = {10.1145/3167080}, PUBLISHER = {ACM}, YEAR = {2018}, DATE = {2018}, BOOKTITLE = {CPP'18, 7th ACM SIGPLAN International Conference on Certified Programs and Proofs}, EDITOR = {Andronick, June and Felty, Amy}, PAGES = {158--171}, ADDRESS = {Los Angeles, CA, USA}, }
Endnote
%0 Conference Proceedings %A Fleury, Mathias %A Blanchette, Jasmin Christian %A Lammich, Peter %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T A Verified SAT Solver with Watched Literals using Imperative HOL : %G eng %U http://hdl.handle.net/21.11116/0000-0001-4174-3 %R 10.1145/3167080 %D 2018 %B 7th ACM SIGPLAN International Conference on Certified Programs and Proofs %Z date of event: 2018-01-08 - 2018-01-09 %C Los Angeles, CA, USA %B CPP'18 %E Andronick, June; Felty, Amy %P 158 - 171 %I ACM %@ 978-1-4503-5586-5
Schlichtkrull, A., Blanchette, J. C., Traytel, D., & Waldmann, U. (2018). Formalization of Bachmair and Ganzinger’s Ordered Resolution Prover. Archive of Formal Proofs.
Export
BibTeX
@article{BlanchetteAFP2018, TITLE = {Formalization 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 = {2150-914X}, YEAR = {2018}, JOURNAL = {Archive of Formal Proofs}, }
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 Formalization of Bachmair and Ganzinger’s Ordered Resolution Prover : %G eng %U http://hdl.handle.net/21.11116/0000-0000-6489-5 %7 2018-01-18 %D 2018 %8 18.01.2018 %J Archive of Formal Proofs %@ false %U https://www.isa-afp.org/browser_info/current/AFP/Ordered_Resolution_Prover/document.pdf
Teucke, A. (2018). An Approximation and Refinement Approach to First-Order Automated Reasoning. Universität des Saarlandes, Saarbrücken. Retrieved from urn:nbn:de:bsz:291-scidok-ds-271963
Abstract
With the goal of lifting model-based guidance from the propositional setting to first- order logic, I have developed an approximation theorem proving approach based on counterexample-guided abstraction refinement. A given clause set is transformed into a simplified form where satisfiability is decidable. This approximation extends the signature and preserves unsatisfiability: if the simplified clause set is satisfi- able, so is the original clause set. A resolution refutation generated by a decision procedure on the simplified clause set can then either be lifted to a refutation in the original clause set, or it guides a refinement excluding the previously found unliftable refutation. This way the approach is refutationally complete. The monadic shallow linear Horn fragment, which is the initial target of the approximation, is well-known to be decidable. It was a long standing open prob- lem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. I have now proven de- cidability of the non-Horn monadic shallow linear fragment via ordered resolution. I further extend the clause language with a new type of constraints, called straight dismatching constraints. The extended clause language is motivated by an improved refinement of the approximation-refinement framework. All needed oper- ations on straight dismatching constraints take linear or linear logarithmic time in the size of the constraint. Ordered resolution with straight dismatching constraints is sound and complete and the monadic shallow linear fragment with straight dis- matching constraints is decidable. I have implemented my approach based on the SPASS theorem prover. On cer- tain satisfiable problems, the implementation shows the ability to beat established provers such as SPASS, iProver, and Vampire.
Export
BibTeX
@phdthesis{Teuckephd2018, TITLE = {An Approximation and Refinement Approach to First-Order Automated Reasoning}, AUTHOR = {Teucke, Andreas}, LANGUAGE = {eng}, URL = {urn:nbn:de:bsz:291-scidok-ds-271963}, DOI = {10.22028/D291-27196}, SCHOOL = {Universit{\"a}t des Saarlandes}, ADDRESS = {Saarbr{\"u}cken}, YEAR = {2018}, DATE = {2018}, ABSTRACT = {With the goal of lifting model-based guidance from the propositional setting to first- order logic, I have developed an approximation theorem proving approach based on counterexample-guided abstraction refinement. A given clause set is transformed into a simplified form where satisfiability is decidable. This approximation extends the signature and preserves unsatisfiability: if the simplified clause set is satisfi- able, so is the original clause set. A resolution refutation generated by a decision procedure on the simplified clause set can then either be lifted to a refutation in the original clause set, or it guides a refinement excluding the previously found unliftable refutation. This way the approach is refutationally complete. The monadic shallow linear Horn fragment, which is the initial target of the approximation, is well-known to be decidable. It was a long standing open prob- lem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. I have now proven de- cidability of the non-Horn monadic shallow linear fragment via ordered resolution. I further extend the clause language with a new type of constraints, called straight dismatching constraints. The extended clause language is motivated by an improved refinement of the approximation-refinement framework. All needed oper- ations on straight dismatching constraints take linear or linear logarithmic time in the size of the constraint. Ordered resolution with straight dismatching constraints is sound and complete and the monadic shallow linear fragment with straight dis- matching constraints is decidable. I have implemented my approach based on the SPASS theorem prover. On cer- tain satisfiable problems, the implementation shows the ability to beat established provers such as SPASS, iProver, and Vampire.}, }
Endnote
%0 Thesis %A Teucke, Andreas %A referee: Korovin, Konstatin %Y Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society International Max Planck Research School, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T An Approximation and Refinement Approach to First-Order Automated Reasoning : %G eng %U http://hdl.handle.net/21.11116/0000-0001-8E49-E %R 10.22028/D291-27196 %U urn:nbn:de:bsz:291-scidok-ds-271963 %I Universität des Saarlandes %C Saarbrücken %D 2018 %P XIV, 133 p. %V phd %9 phd %X With the goal of lifting model-based guidance from the propositional setting to first- order logic, I have developed an approximation theorem proving approach based on counterexample-guided abstraction refinement. A given clause set is transformed into a simplified form where satisfiability is decidable. This approximation extends the signature and preserves unsatisfiability: if the simplified clause set is satisfi- able, so is the original clause set. A resolution refutation generated by a decision procedure on the simplified clause set can then either be lifted to a refutation in the original clause set, or it guides a refinement excluding the previously found unliftable refutation. This way the approach is refutationally complete. The monadic shallow linear Horn fragment, which is the initial target of the approximation, is well-known to be decidable. It was a long standing open prob- lem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. I have now proven de- cidability of the non-Horn monadic shallow linear fragment via ordered resolution. I further extend the clause language with a new type of constraints, called straight dismatching constraints. The extended clause language is motivated by an improved refinement of the approximation-refinement framework. All needed oper- ations on straight dismatching constraints take linear or linear logarithmic time in the size of the constraint. Ordered resolution with straight dismatching constraints is sound and complete and the monadic shallow linear fragment with straight dis- matching constraints is decidable. I have implemented my approach based on the SPASS theorem prover. On cer- tain satisfiable problems, the implementation shows the ability to beat established provers such as SPASS, iProver, and Vampire. %U https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/27069