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}, MARGINALMARK = {$\bullet$}, 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
Bentkamp, A., Blanchette, J. C., Cruanes, S., & Waldmann, U. (2018). Superposition for Lambda-Free Higher-Order Logic. In Automated Reasoning (IJCAR 2018). Oxford, UK: Springer. doi:10.1007/978-3-319-94205-6_3
Export
BibTeX
@inproceedings{Bentkamp_IJCAR2018, TITLE = {Superposition for Lambda-Free Higher-Order Logic}, AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin Christian and Cruanes, Simon and Waldmann, Uwe}, LANGUAGE = {eng}, ISBN = {978-3-319-94204-9}, DOI = {10.1007/978-3-319-94205-6_3}, PUBLISHER = {Springer}, YEAR = {2018}, MARGINALMARK = {$\bullet$}, DATE = {2018}, BOOKTITLE = {Automated Reasoning (IJCAR 2018)}, EDITOR = {Galmiche, Didier and Schulz, Stephan and Sebastiani, Roberto}, PAGES = {28--46}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {10900}, ADDRESS = {Oxford, UK}, }
Endnote
%0 Conference Proceedings %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Cruanes, Simon %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 Superposition for Lambda-Free Higher-Order Logic : %G eng %U http://hdl.handle.net/21.11116/0000-0002-5F3A-4 %R 10.1007/978-3-319-94205-6_3 %D 2018 %B 9th International Joint Conference on Automated Reasoning %Z date of event: 2018-07-14 - 2018-07-17 %C Oxford, UK %B Automated Reasoning %E Galmiche, Didier; Schulz, Stephan; Sebastiani, Roberto %P 28 - 46 %I Springer %@ 978-3-319-94204-9 %B Lecture Notes in Artificial Intelligence %N 10900
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}, MARGINALMARK = {$\bullet$}, 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
Blanchette, J. C., Peltier, N., & Robillard, S. (2018). Superposition with Datatypes and Codatatypes. In Automated Reasoning (IJCAR 2018). Oxford, UK: Springer. doi:10.1007/978-3-319-94205-6_25
Export
BibTeX
@inproceedings{Blanchette_IJCAR2018, TITLE = {Superposition with Datatypes and Codatatypes}, AUTHOR = {Blanchette, Jasmin Christian and Peltier, Nicolas and Robillard, Simon}, LANGUAGE = {eng}, ISBN = {978-3-319-94204-9}, DOI = {10.1007/978-3-319-94205-6_25}, PUBLISHER = {Springer}, YEAR = {2018}, MARGINALMARK = {$\bullet$}, DATE = {2018}, BOOKTITLE = {Automated Reasoning (IJCAR 2018)}, EDITOR = {Galmiche, Didier and Schulz, Stephan and Sebastiani, Roberto}, PAGES = {370--387}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {10900}, ADDRESS = {Oxford, UK}, }
Endnote
%0 Conference Proceedings %A Blanchette, Jasmin Christian %A Peltier, Nicolas %A Robillard, Simon %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Superposition with Datatypes and Codatatypes : %G eng %U http://hdl.handle.net/21.11116/0000-0002-5F40-C %R 10.1007/978-3-319-94205-6_25 %D 2018 %B 9th International Joint Conference on Automated Reasoning %Z date of event: 2018-07-14 - 2018-07-17 %C Oxford, UK %B Automated Reasoning %E Galmiche, Didier; Schulz, Stephan; Sebastiani, Roberto %P 370 - 387 %I Springer %@ 978-3-319-94204-9 %B Lecture Notes in Artificial Intelligence %N 10900
Bromberger, M. (2018). A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems. In Automated Reasoning (IJCAR 2018). Oxford, UK: Springer. doi:10.1007/978-3-319-94205-6_22
Export
BibTeX
@inproceedings{Bromberger18, TITLE = {A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems}, AUTHOR = {Bromberger, Martin}, LANGUAGE = {eng}, ISBN = {978-3-319-94204-9}, DOI = {10.1007/978-3-319-94205-6_22}, PUBLISHER = {Springer}, YEAR = {2018}, MARGINALMARK = {$\bullet$}, DATE = {2018}, BOOKTITLE = {Automated Reasoning (IJCAR 2018)}, EDITOR = {Galmiche, Didier and Schulz, Stephan and Sebastiani, Roberto}, PAGES = {329--345}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {10900}, ADDRESS = {Oxford, UK}, }
Endnote
%0 Conference Proceedings %A Bromberger, Martin %+ Automation of Logic, MPI for Informatics, Max Planck Society %T A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems : %G eng %U http://hdl.handle.net/21.11116/0000-0002-94C1-C %R 10.1007/978-3-319-94205-6_22 %D 2018 %B 9th International Joint Conference on Automated Reasoning %Z date of event: 2018-07-14 - 2018-07-17 %C Oxford, UK %B Automated Reasoning %E Galmiche, Didier; Schulz, Stephan; Sebastiani, Roberto %P 329 - 345 %I Springer %@ 978-3-319-94204-9 %B Lecture Notes in Artificial Intelligence %N 10900
Cropper, A., & Tourret, S. (2018). Derivation Reduction of Metarules in Meta-interpretive Learning. In Inductive Logic Programming (ILP 2018). Ferrara, Italy: Springer. doi:10.1007/978-3-319-99960-9_1
Export
BibTeX
@inproceedings{Cropper_ILP2018, TITLE = {Derivation Reduction of Metarules in Meta-interpretive Learning}, AUTHOR = {Cropper, Andrew and Tourret, Sophie}, LANGUAGE = {eng}, ISBN = {978-3-319-99959-3; 978-3-319-99960-9}, DOI = {10.1007/978-3-319-99960-9_1}, PUBLISHER = {Springer}, YEAR = {2018}, MARGINALMARK = {$\bullet$}, DATE = {2018}, BOOKTITLE = {Inductive Logic Programming (ILP 2018)}, EDITOR = {Riguzi, Fabrizio and Bellodi, Elena and Zese, Riccardo}, PAGES = {1--21}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {11105}, ADDRESS = {Ferrara, Italy}, }
Endnote
%0 Conference Proceedings %A Cropper, Andrew %A Tourret, Sophie %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Derivation Reduction of Metarules in Meta-interpretive Learning : %G eng %U http://hdl.handle.net/21.11116/0000-0002-A2B9-6 %R 10.1007/978-3-319-99960-9_1 %D 2018 %B 28th International Conference on Inductive Logic Programming %Z date of event: 2018-09-02 - 2018-09-04 %C Ferrara, Italy %B Inductive Logic Programming %E Riguzi, Fabrizio; Bellodi, Elena; Zese, Riccardo %P 1 - 21 %I Springer %@ 978-3-319-99959-3 978-3-319-99960-9 %B Lecture Notes in Artificial Intelligence %N 11105
Echenim, M., Peltier, N., & Tourret, S. (2018). Prime Implicate Generation in Equational Logic. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI 2018). Stockholm, Sweden: IJCAI. doi:10.24963/ijcai.2018/790
Export
BibTeX
@inproceedings{EchenimIJCAI2018, TITLE = {Prime Implicate Generation in Equational Logic}, AUTHOR = {Echenim, Mnacho and Peltier, Nicolas and Tourret, Sophie}, LANGUAGE = {eng}, ISBN = {978-0-9992411-2-7}, DOI = {10.24963/ijcai.2018/790}, PUBLISHER = {IJCAI}, YEAR = {2018}, MARGINALMARK = {$\bullet$}, BOOKTITLE = {Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI 2018)}, EDITOR = {Lang, J{\'e}r{\^o}me}, PAGES = {5588--5592}, ADDRESS = {Stockholm, Sweden}, }
Endnote
%0 Conference Proceedings %A Echenim, Mnacho %A Peltier, Nicolas %A Tourret, Sophie %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Prime Implicate Generation in Equational Logic : %G eng %U http://hdl.handle.net/21.11116/0000-0002-A2B1-E %R 10.24963/ijcai.2018/790 %D 2018 %B 27th International Joint Conference on Artificial Intelligence and the 23rd European Conference on Artificial Intelligence %Z date of event: 2018-07-13 - 2018-07-19 %C Stockholm, Sweden %B Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence %E Lang, Jérôme %P 5588 - 5592 %I IJCAI %@ 978-0-9992411-2-7
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}, MARGINALMARK = {$\bullet$}, 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
Hong, H., & Sturm, T. (2018a). Positive Solutions of Systems of Signed Parametric Polynomial Inequalities. Retrieved from http://arxiv.org/abs/1804.09705
(arXiv: 1804.09705)
Abstract
We consider systems of strict multivariate polynomial inequalities over the reals. All polynomial coefficients are parameters ranging over the reals, where for each coefficient we prescribe its sign. We are interested in the existence of positive real solutions of our system for all choices of coefficients subject to our sign conditions. We give a decision procedure for the existence of such solutions. In the positive case our procedure yields a parametric positive solution as a rational function in the coefficients. Our framework allows to reformulate heuristic subtropical approaches for non-parametric systems of polynomial inequalities that have been recently used in qualitative biological network analysis and, independently, in satisfiability modulo theory solving. We apply our results to characterize the incompleteness of those methods.
Export
BibTeX
@online{Hong_arXiv1804.09705, TITLE = {Positive Solutions of Systems of Signed Parametric Polynomial Inequalities}, AUTHOR = {Hong, Hoon and Sturm, Thomas}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1804.09705}, EPRINT = {1804.09705}, EPRINTTYPE = {arXiv}, YEAR = {2018}, MARGINALMARK = {$\bullet$}, ABSTRACT = {We consider systems of strict multivariate polynomial inequalities over the reals. All polynomial coefficients are parameters ranging over the reals, where for each coefficient we prescribe its sign. We are interested in the existence of positive real solutions of our system for all choices of coefficients subject to our sign conditions. We give a decision procedure for the existence of such solutions. In the positive case our procedure yields a parametric positive solution as a rational function in the coefficients. Our framework allows to reformulate heuristic subtropical approaches for non-parametric systems of polynomial inequalities that have been recently used in qualitative biological network analysis and, independently, in satisfiability modulo theory solving. We apply our results to characterize the incompleteness of those methods.}, }
Endnote
%0 Report %A Hong, Hoon %A Sturm, Thomas %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Positive Solutions of Systems of Signed Parametric Polynomial Inequalities : %G eng %U http://hdl.handle.net/21.11116/0000-0002-5F54-6 %U http://arxiv.org/abs/1804.09705 %D 2018 %X We consider systems of strict multivariate polynomial inequalities over the reals. All polynomial coefficients are parameters ranging over the reals, where for each coefficient we prescribe its sign. We are interested in the existence of positive real solutions of our system for all choices of coefficients subject to our sign conditions. We give a decision procedure for the existence of such solutions. In the positive case our procedure yields a parametric positive solution as a rational function in the coefficients. Our framework allows to reformulate heuristic subtropical approaches for non-parametric systems of polynomial inequalities that have been recently used in qualitative biological network analysis and, independently, in satisfiability modulo theory solving. We apply our results to characterize the incompleteness of those methods. %K Computer Science, Symbolic Computation, cs.SC,Computer Science, Logic in Computer Science, cs.LO
Hong, H., & Sturm, T. (2018b). Positive Solutions of Systems of Signed Parametric Polynomial Inequalities. In Computer Algebra in Scientific Computing (CASC 2018). Lille, France: Springer. doi:10.1007/978-3-319-99639-4_17
Export
BibTeX
@inproceedings{Hong_CASC2018, TITLE = {Positive Solutions of Systems of Signed Parametric Polynomial Inequalities}, AUTHOR = {Hong, Hoon and Sturm, Thomas}, LANGUAGE = {eng}, ISBN = {978-3-319-99638-7}, DOI = {10.1007/978-3-319-99639-4_17}, PUBLISHER = {Springer}, YEAR = {2018}, MARGINALMARK = {$\bullet$}, DATE = {2018}, BOOKTITLE = {Computer Algebra in Scientific Computing (CASC 2018)}, EDITOR = {Gerdt, Vladimir P. and Koepf, Wolfram and Seiler, Werner M. and Vorozhtsov, Evgenii V.}, PAGES = {238--253}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {11077}, ADDRESS = {Lille, France}, }
Endnote
%0 Conference Proceedings %A Hong, Hoon %A Sturm, Thomas %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Positive Solutions of Systems of Signed Parametric Polynomial Inequalities : %G eng %U http://hdl.handle.net/21.11116/0000-0002-5F60-8 %R 10.1007/978-3-319-99639-4_17 %D 2018 %B 20th International Workshop on Computer Algebra in Scientific Computing %Z date of event: 2018-09-17 - 2018-09-21 %C Lille, France %B Computer Algebra in Scientific Computing %E Gerdt, Vladimir P.; Koepf, Wolfram; Seiler, Werner M.; Vorozhtsov, Evgenii V. %P 238 - 253 %I Springer %@ 978-3-319-99638-7 %B Lecture Notes in Computer Science %N 11077
Schlichtkrull, A., Blanchette, J. C., Traytel, D., & Waldmann, U. (2018a). 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}, MARGINALMARK = {$\bullet$}, 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
Schlichtkrull, A., Blanchette, J. C., Traytel, D., & Waldmann, U. (2018b). Formalization of Bachmair and Ganzinger’s Ordered Resolution Prover. In Automated Reasoning (IJCAR 2018). Oxford, UK: Springer. doi:10.1007/978-3-319-94205-6_7
Export
BibTeX
@inproceedings{Schlichtkrull_IJCAR2018, 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}, ISBN = {978-3-319-94204-9}, DOI = {10.1007/978-3-319-94205-6_7}, PUBLISHER = {Springer}, YEAR = {2018}, MARGINALMARK = {$\bullet$}, DATE = {2018}, BOOKTITLE = {Automated Reasoning (IJCAR 2018)}, EDITOR = {Galmiche, Didier and Schulz, Stephan and Sebastiani, Roberto}, PAGES = {89--107}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {10900}, ADDRESS = {Oxford, UK}, }
Endnote
%0 Conference Proceedings %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-0002-5F3E-0 %R 10.1007/978-3-319-94205-6_7 %D 2018 %B 9th International Joint Conference on Automated Reasoning %Z date of event: 2018-07-14 - 2018-07-17 %C Oxford, UK %B Automated Reasoning %E Galmiche, Didier; Schulz, Stephan; Sebastiani, Roberto %P 89 - 107 %I Springer %@ 978-3-319-94204-9 %B Lecture Notes in Artificial Intelligence %N 10900
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}, MARGINALMARK = {$\bullet$}, 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