Publications

%0 Journal Article %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Tourret, Sophie %A Vukmirović, Petar %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Superposition for Higher-Order Logic : %G eng %U http://hdl.handle.net/21.11116/0000-000C-C5EB-D %R 10.1007/s10817-022-09649-9 %7 2023 %D 2023 %J Journal of Automated Reasoning %V 67 %N 1 %Z sequence number: 10 %I D. Reidel Pub. Co. %C Dordrecht, Holland %@ false

%0 Report %A Bromberger, Martin %A Schwarz, Simon %A Weidenbach, Christoph %+ 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 SCL(FOL) Revisited : %G eng %U http://hdl.handle.net/21.11116/0000-000C-C3B4-C %U https://arxiv.org/abs/2302.05954 %D 2023 %X This paper presents an up-to-date and refined version of the SCL calculus for<br>first-order logic without equality. The refinement mainly consists of the<br>following two parts: First, we incorporate a stronger notion of regularity into<br>SCL(FOL). Our regularity definition is adapted from the SCL(T) calculus. This<br>adapted definition guarantees non-redundant clause learning during a run of<br>SCL. However, in contrast to the original presentation, it does not require<br>exhaustive propagation. Second, we introduce trail and model bounding to<br>achieve termination guarantees. In previous versions, no termination guarantees<br>about SCL were achieved. Last, we give rigorous proofs for soundness,<br>completeness and clause learning guarantees of SCL(FOL) and put SCL(FOL) into<br>context of existing first-order calculi.<br> %K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Symbolic Computation, cs.SC

%0 Journal Article %A Akbarbaglu, Ibrahim %A Aghababa, Hasan P. %A Rahkooy, Hamid %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T On the Algebraic Structures in A(Phi) (G) : %G eng %U http://hdl.handle.net/21.11116/0000-000A-A750-F %R 10.1007/s00009-022-02052-z %7 2022 %D 2022 %J Mediterranian Journal of Mathematics %V 19 %N 3 %Z sequence number: 131 %I Springer %C New York, NY

%0 Report %A Blanchette, Jasmin Christian %A Vukmirovi&#263;, Petar %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T SAT-Inspired Higher-Order Eliminations : %G eng %U http://hdl.handle.net/21.11116/0000-000B-653C-1 %U https://arxiv.org/abs/2208.07775 %D 2022 %X We generalize several propositional preprocessing techniques to higher-order<br>logic, building on existing first-order generalizations. These techniques<br>eliminate literals, clauses, or predicate symbols from the problem, with the<br>aim of making it more amenable to automatic proof search. We also introduce a<br>new technique, which we call quasipure literal elimination, that strictly<br>subsumes pure literal elimination. The new techniques are implemented in the<br>Zipperposition theorem prover. Our evaluation shows that they sometimes help<br>prove problems originating from the TPTP library and Isabelle formalizations.<br> %K Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A Bromberger, Martin %A Gehl, Tobias %A Leutgeb, Lorenz %A Weidenbach, Christoph %+ 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 A Two-Watched Literal Scheme for First-Order Logic : %G eng %U http://hdl.handle.net/21.11116/0000-000B-63DF-B %U https://ceur-ws.org/Vol-3201/paper2.pdf %D 2022 %B Practical Aspects of Automated Reasoning 2022 %Z date of event: 2022-08-11 - 2022-08-12 %C Haifa, Israel %B Practical Aspects of Automated Reasoning 2022 %E Konev, Boris; Schon, Claudia; Steen, Alexander %I CEUR-WS.org %B CEUR Workshop Proceedings %N 3201 %@ false

%0 Conference Proceedings %A Bromberger, Martin %A Leutgeb, Lorenz %A Weidenbach, Christoph %+ 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 An Efficient Subsumption Test Pipeline for BS(LRA) Clauses : %G eng %U http://hdl.handle.net/21.11116/0000-000B-639F-3 %R 10.1007/978-3-031-10769-6_10 %U https://rdcu.be/cY8Pp %D 2022 %B 11th International Joint Conference on Automated Reasoning %Z date of event: 2022-08-08 - 2022-08-10 %C Haifa, Israel %B Automated Reasoning %E Blanchette, Jasmin Christian; Kov&#225;cs, Laura; Pattinson, Dirk %P 147 - 168 %I Springer %@ 978-3-031-10768-9 %B Lecture Notes in Artificial Intelligence %N 13385

%0 Conference Proceedings %A Bromberger, Martin %A Schwarz, Simon %A Weidenbach, Christoph %+ 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 Exploring Partial Models with SCL : %G eng %U http://hdl.handle.net/21.11116/0000-000B-63E5-3 %U https://ceur-ws.org/Vol-3201/paper5.pdf %D 2022 %B Practical Aspects of Automated Reasoning 2022 %Z date of event: 2022-08-11 - 2022-08-12 %C Haifa, Israel %B Practical Aspects of Automated Reasoning 2022 %E Konev, Boris; Schon, Claudia; Steen, Alexander %I CEUR-WS.org %B CEUR Workshop Proceedings %N 3201 %@ false

%0 Report %A Bromberger, Martin %A Dragoste, Irina %A Faqeh, Rasha %A Fetzer, Christof %A Gonz&#225;lez, Larry %A Kr&#246;tzsch, Markus %A Marx, Maximilian %A Murali, Harish K. %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic : %G eng %U http://hdl.handle.net/21.11116/0000-000B-652B-4 %U https://arxiv.org/abs/2201.09769 %D 2022 %X In a previous paper, we have shown that clause sets belonging to the Horn<br>Bernays-Sch\"onfinkel fragment over simple linear real arithmetic (HBS(SLR))<br>can be translated into HBS clause sets over a finite set of first-order<br>constants. The translation preserves validity and satisfiability and it is<br>still applicable if we extend our input with positive universally or<br>existentially quantified verification conditions (conjectures). We call this<br>translation a Datalog hammer. The combination of its implementation in<br>SPASS-SPL with the Datalog reasoner VLog establishes an effective way of<br>deciding verification conditions in the Horn fragment. We verify supervisor<br>code for two examples: a lane change assistant in a car and an electronic<br>control unit of a supercharged combustion engine. In this paper, we improve our<br>Datalog hammer in several ways: we generalize it to mixed real-integer<br>arithmetic and finite first-order sorts; we extend the class of acceptable<br>inequalities beyond variable bounds and positively grounded inequalities; and<br>we significantly reduce the size of the hammer output by a soft typing<br>discipline. We call the result the sorted Datalog hammer. It not only allows us<br>to handle more complex supervisor code and to model already considered<br>supervisor code more concisely, but it also improves our performance on real<br>world benchmark examples. Finally, we replace the before file-based interface<br>between SPASS-SPL and VLog by a close coupling resulting in a single executable<br>binary.<br> %K Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A Bromberger, Martin %A Dragoste, Irina %A Faqeh, Rasha %A Fetzer, Christof %A Gonz&#225;lez, Larry %A Kr&#246;tzsch, Markus %A Marx, Maximilian %A Murali, Harish K. %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic : %G eng %U http://hdl.handle.net/21.11116/0000-000B-6527-8 %R 10.1007/978-3-030-99524-9_27 %D 2022 %B 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems %Z date of event: 2022-04-02 - 2022-04-07 %C Munich, Germany %B Tools and Algorithms for the Construction and Analysis of Systems %E Fisman, Dana; Rosu, Grigore %P 480 - 501 %I Springer %@ 978-3-030-99523-2 %B Lecture Notes in Computer Science %N 13243

%0 Conference Proceedings %A Demin, Alexander %A Rahkooy, Hamid %A Sturm, Thomas %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T F5: A REDUCE Package for Signature-based Gr&#246;bner Basis Computation : %G eng %U http://hdl.handle.net/21.11116/0000-000C-BE85-8 %F OTHER: hal-03781962 %U https://hal.science/hal-03781962 %D 2022 %B 24th International Workshop on Computer Algebra in Scientific Computing %Z date of event: 2022-08-22 - 2022-08-26 %C Gebze, Turkey %B CASC 2022 - Computer Algebra in Scientific Computing %I HAL

%0 Conference Proceedings %A Desharnais, Martin %A Vukmirovi&#263;, Petar %A Blanchette, Jasmin Christian %A Wenzel, Makarius %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Seventeen Provers Under the Hammer : %G eng %U http://hdl.handle.net/21.11116/0000-000B-6539-4 %R 10.4230/LIPIcs.ITP.2022.8 %U urn:nbn:de:0030-drops-167178 %D 2022 %B 13th International Conference on Interactive Theorem Proving %Z date of event: 2022-08-07 - 2022-08-10 %C Haifa, Israel %B 13th International Conference on Interactive Theorem Proving %E Andronick, June; Moura, Leonardo %P 118 - 87 %Z sequence number: 8 %I Schloss Dagstuhl %@ 978-3-95977-252-5 %B Leibniz International Proceedings in Informatics %N 237 %U https://drops.dagstuhl.de/opus/volltexte/2022/16717https://doi.org/10.5281/zenodo.5940084

%0 Journal Article %A Frohn, Florian %A Fuhs, Carsten %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T A Calculus for Modular Loop Acceleration and Non-Termination Proofs : %G eng %U http://hdl.handle.net/21.11116/0000-000B-58D4-3 %R 10.1007/s10009-022-00670-2 %7 2022 %D 2022 %J International Journal on Software Tools for Technology Transfer %O STTT %V 24 %& 691 %P 691 - 715 %I Springer %C Berlin %@ false

%0 Conference Proceedings %A Haifani, Fajar %A Koopmann, Patrick %A Tourret, Sophie %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Connection-Minimal Abduction in EL via Translation to FOL (Extended Abstract) : %G eng %U http://hdl.handle.net/21.11116/0000-000B-6558-1 %U https://ceur-ws.org/Vol-3263/abstract-12.pdf %D 2022 %B 35th International Workshop on Description Logics %Z date of event: 2022-08-07 - 2022-08-10 %C Haifa, Israel %B Description Logics 2022 %E Arieli, Ofer; Homola, Martin; Jung, Jean Christoph; Mugnier, Marie-Laure %I CEUR-WS.org %B CEUR Workshop Proceedings %N 3263 %@ false

%0 Conference Proceedings %A Haifani, Fajar %A Koopmann, Patrick %A Tourret, Sophie %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Connection-Minimal Abduction in EL via Translation to FOL : %G eng %U http://hdl.handle.net/21.11116/0000-000B-63BE-0 %R 10.1007/978-3-031-10769-6_12 %U https://rdcu.be/cY8T3 %D 2022 %B 11th International Joint Conference on Automated Reasoning %Z date of event: 2022-08-08 - 2022-08-10 %C Haifa, Israel %B Automated Reasoning %E Blanchette, Jasmin Christian; Kov&#225;cs, Laura; Pattinson, Dirk %P 188 - 207 %I Springer %@ 978-3-031-10768-9 %B Lecture Notes in Artificial Intelligence %N 13385

%0 Conference Proceedings %A Haifani, Fajar %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Semantic Relevance : %G eng %U http://hdl.handle.net/21.11116/0000-000B-63C9-3 %R 10.1007/978-3-031-10769-6_13 %U https://rdcu.be/cY8UF %D 2022 %B 11th International Joint Conference on Automated Reasoning %Z date of event: 2022-08-08 - 2022-08-10 %C Haifa, Israel %B Automated Reasoning %E Blanchette, Jasmin Christian; Kov&#225;cs, Laura; Pattinson, Dirk %P 208 - 227 %I Springer %@ 978-3-031-10768-9 %B Lecture Notes in Artificial Intelligence %N 13385

%0 Report %A Haifani, Fajar %A Koopmann, Patrick %A Tourret, Sophie %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Connection-minimal Abduction in EL via Translation to FOL -- Technical Report : %G eng %U http://hdl.handle.net/21.11116/0000-000B-6531-C %U https://arxiv.org/abs/2205.08449 %D 2022 %X Abduction in description logics finds extensions of a knowledge base to make<br>it entail an observation. As such, it can be used to explain why the<br>observation does not follow, to repair incomplete knowledge bases, and to<br>provide possible explanations for unexpected observations. We consider TBox<br>abduction in the lightweight description logic EL, where the observation is a<br>concept inclusion and the background knowledge is a TBox, i.e., a set of<br>concept inclusions. To avoid useless answers, such problems usually come with<br>further restrictions on the solution space and/or minimality criteria that help<br>sort the chaff from the grain. We argue that existing minimality notions are<br>insufficient, and introduce connection minimality. This criterion follows<br>Occam's razor by rejecting hypotheses that use concept inclusions unrelated to<br>the problem at hand. We show how to compute a special class of<br>connection-minimal hypotheses in a sound and complete way. Our technique is<br>based on a translation to first-order logic, and constructs hypotheses based on<br>prime implicates. We evaluate a prototype implementation of our approach on<br>ontologies from the medical domain.<br> %K Computer Science, Artificial Intelligence, cs.AI,Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A Leidinger, Hendrik %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T SCL(EQ): SCL for First-Order Logic with Equality : %G eng %U http://hdl.handle.net/21.11116/0000-000B-63D4-6 %R 10.1007/978-3-031-10769-6_14 %U https://rdcu.be/cY8VZ %D 2022 %B 11th International Joint Conference on Automated Reasoning %Z date of event: 2022-08-08 - 2022-08-10 %C Haifa, Israel %B Automated Reasoning %E Blanchette, Jasmin Christian; Kov&#225;cs, Laura; Pattinson, Dirk %P 228 - 247 %I Springer %@ 978-3-031-10768-9 %B Lecture Notes in Artificial Intelligence %N 13385

%0 Report %A Leidinger, Hendrik %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T SCL(EQ): SCL for First-Order Logic with Equality : %G eng %U http://hdl.handle.net/21.11116/0000-000B-652E-1 %U https://arxiv.org/abs/2205.08297 %D 2022 %X We propose a new calculus SCL(EQ) for first-order logic with equality that<br>only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven<br>Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal<br>model assumption is used to guide inferences that are then guaranteed to be<br>non-redundant. Redundancy is defined with respect to a dynamically changing<br>ordering derived from the ground literal model assumption. We prove SCL(EQ)<br>sound and complete and provide examples where our calculus improves on<br>superposition.<br> %K Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A Leutgeb, Lorenz %A Moser, Georg %A Zuleger, Florian %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Automated Expected Amortised Cost Analysis of Probabilistic Data Structures : %G eng %U http://hdl.handle.net/21.11116/0000-000B-CA5F-8 %R 10.1007/978-3-031-13188-2_4 %U https://rdcu.be/c1faB %D 2022 %B 34th International Conference on Computer-Aided Verification %Z date of event: 2022-08-07 - 2022-08-10 %C Haifa, Israel %B Computer Aided Verification %E Shoham, Sharon; Vizel, Yakir %P 70 - 91 %I Springer %@ 978-3-031-13187-5 %B Lecture Notes in Computer Science %N 13372

%0 Report %A L&#252;ders, Christoph %A Sturm, Thomas %A Radulescu, Ovidiu %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T ODEbase: A Repository of ODE Systems for Systems Biology : %G eng %U http://hdl.handle.net/21.11116/0000-000B-654F-C %U https://arxiv.org/abs/2201.08980 %D 2022 %X Recently, symbolic computation and computer algebra systems have been<br>successfully applied in systems biology, especially in chemical reaction<br>network theory. One advantage of symbolic computation is its potential for<br>qualitative answers to biological questions. Qualitative methods analyze<br>dynamical input systems as formal objects, in contrast to investigating only<br>part of the state space, as is the case with numerical simulation. However,<br>symbolic computation tools and libraries have a different set of requirements<br>for their input data than their numerical counterparts. A common format used in<br>mathematical modeling of biological processes is SBML. We illustrate that the<br>use of SBML data in symbolic computation requires significant pre-processing,<br>incorporating external biological and mathematical expertise. ODEbase provides<br>high quality symbolic computation input data derived from established existing<br>biomodels, covering in particular the BioModels database.<br> %K Quantitative Biology, Molecular Networks, q-bio.MN,Computer Science, Symbolic Computation, cs.SC

%0 Journal Article %A L&#252;ders, Christoph %A Sturm, Thomas %A Radulescu, Ovidiu %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T ODEbase: A Repository of ODE Systems for Systems Biology : %G eng %U http://hdl.handle.net/21.11116/0000-000C-BE66-C %R 10.1093/bioadv/vbac027 %7 2022 %D 2022 %J Bioinformatics Advances %V 2 %N 2 %Z sequence number: vbac027 %I Oxford University Press %C Oxford %@ false

%0 Journal Article %A Tourret, Sophie %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column : %G eng %U http://hdl.handle.net/21.11116/0000-0009-FACB-9 %R 10.1007/s10817-022-09617-3 %7 2022 %D 2022 %J Journal of Automated Reasoning %V 66 %& 575 %P 575 - 584 %I Springer %C New York, NY %@ false

%0 Journal Article %A Vukmirovi&#263;, Petar %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Cruanes, Simon %A Nummelin, Visa %A Tourret, Sophie %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Making Higher-Order Superposition Work : %G eng %U http://hdl.handle.net/21.11116/0000-0009-F7A1-A %R 10.1007/s10817-021-09613-z %7 2022 %D 2022 %J Journal of Automated Reasoning %V 66 %& 541 %P 541 - 564 %I Springer %C New York, NY %@ false %U https://rdcu.be/cGXwx

%0 Journal Article %A Vukmirovi&#263;, Petar %A Blanchette, Jasmin Christian %A Cruanes, Simon %A Schulz, Stephan %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Extending a Brainiac Prover to Lambda-Free Higher-Order Logic : %G eng %U http://hdl.handle.net/21.11116/0000-0009-2A64-8 %R 10.1007/s10009-021-00639-7 %7 2021 %D 2022 %J International Journal on Software Tools for Technology Transfer (STTT) %V 24 %& 67 %P 67 - 87 %I Springer %C Berlin %@ false

%0 Journal Article %A Waldmann, Uwe %A Tourret, Sophie %A Robillard, Simon %A Blanchette, Jasmin Christian %+ 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 Comprehensive Framework for Saturation Theorem Proving : %G eng %U http://hdl.handle.net/21.11116/0000-000A-9D8A-A %R 10.1007/s10817-022-09621-7 %7 2022 %D 2022 %J Journal of Automated Reasoning %V 66 %& 499 %P 499 - 539 %I Springer %C New York, NY %@ false

%0 Journal Article %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Tourret, Sophie %A Vukmirovi&#263;, Petar %A Waldmann, Uwe %+ External Organizations 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 Superposition with Lambdas : %G eng %U http://hdl.handle.net/21.11116/0000-0009-2B35-C %R 10.1007/s10817-021-09595-y %7 2021 %D 2021 %J Journal of Automated Reasoning %V 65 %& 893 %P 893 - 940 %I Springer %C New York, NY %@ false

%0 Conference Proceedings %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Tourret, Sophie %A Vukmirovi&#263;, Petar %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Superposition for Full Higher-order Logic : %G eng %U http://hdl.handle.net/21.11116/0000-0009-3F7F-4 %R 10.1007/978-3-030-79876-5_23 %D 2021 %B 28th International Conference on Automated Deduction %Z date of event: 2021-07-12 - 2021-07-15 %C Virtual Event %B Automated Deduction - CADE 28 %E Platzer, Andr&#233;; Sutcliffe, Geof %P 396 - 412 %I Springer %@ 978-3-030-79875-8 %B Lecture Notes in Artificial Intelligence %N 12699

%0 Report %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Tourret, Sophie %A Vukmirovi&#263;, Petar %A Waldmann, Uwe %+ External Organizations 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 Superposition with Lambdas : %G eng %U http://hdl.handle.net/21.11116/0000-0008-0A44-1 %U https://arxiv.org/abs/2102.00453 %D 2021 %X We designed a superposition calculus for a clausal fragment of extensional<br>polymorphic higher-order logic that includes anonymous functions but excludes<br>Booleans. The inference rules work on $\beta\eta$-equivalence classes of<br>$\lambda$-terms and rely on higher-order unification to achieve refutational<br>completeness. We implemented the calculus in the Zipperposition prover and<br>evaluated it on TPTP and Isabelle benchmarks. The results suggest that<br>superposition is a suitable basis for higher-order reasoning.<br> %K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Artificial Intelligence, cs.AI

%0 Journal Article %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Cruanes, Simon %A Waldmann, Uwe %+ External Organizations External Organizations 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-0009-4AC7-4 %R 10.23638/LMCS-17(2:1)2021 %7 2021 %D 2021 %J Logical Methods in Computer Science %V 17 %N 2 %& 1 %P 1 - 38 %Z sequence number: 1 %I https://lmcs.episciences.org

%0 Conference Proceedings %A Bromberger, Martin %A Fiori, Alberto %A Weidenbach, Christoph %+ 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 Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7C49-D %R 10.1007/978-3-030-67067-2_23 %D 2021 %B 22nd International Conference on Verification, Model Checking, and Abstract Interpretation %Z date of event: 2021-01-17 - 2021-01-19 %C Copenhagen, Denmark (Online) %B Verification, Model Checking, and Abstract Interpretation %E Henglein, Fritz; Shoham, Sharon; Yakir, Vizel %P 511 - 533 %I Springer %@ 978-3-030-67066-5 %B Lecture Notes in Computer Science %N 12597

%0 Conference Proceedings %A Bromberger, Martin %A Dragoste, Irina %A Faqeh, Rasha %A Fetzer, Christof %A Kr&#246;tzsch, Markus %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic : %G eng %U http://hdl.handle.net/21.11116/0000-0009-4A0D-7 %D 2021 %B 13th International Symposium on Frontiers of Combining Systems %Z date of event: 2021-09-08 - 2021-09-10 %C Birmingham, UK %B Frontiers of Combining Systems %E Konev, Boris; Reger, Giles %P 3 - 24 %I Springer %@ 978-3-030-86204-6 %B Lecture Notes in Artificial Intelligence %N 12941

%0 Report %A Bromberger, Martin %A Dragoste, Irina %A Faqeh, Rasha %A Fetzer, Christof %A Kr&#246;tzsch, Markus %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic : %G eng %U http://hdl.handle.net/21.11116/0000-0009-4A01-3 %U https://arxiv.org/abs/2107.03189 %D 2021 %X The Bernays-Sch\"onfinkel first-order logic fragment over simple linear real<br>arithmetic constraints BS(SLR) is known to be decidable. We prove that BS(SLR)<br>clause sets with both universally and existentially quantified verification<br>conditions (conjectures) can be translated into BS(SLR) clause sets over a<br>finite set of first-order constants. For the Horn case, we provide a Datalog<br>hammer preserving validity and satisfiability. A toolchain from the BS(LRA)<br>prover SPASS-SPL to the Datalog reasoner VLog establishes an effective way of<br>deciding verification conditions in the Horn fragment. This is exemplified by<br>the verification of supervisor code for a lane change assistant in a car and of<br>an electronic control unit for a supercharged combustion engine.<br> %K Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A Ebner, Gabriel %A Blanchette, Jasmin Christian %A Tourret, Sophie %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T A Unifying Splitting Framework : %G eng %U http://hdl.handle.net/21.11116/0000-0009-3F87-9 %R 10.1007/978-3-030-79876-5_20 %D 2021 %B 28th International Conference on Automated Deduction %Z date of event: 2021-07-12 - 2021-07-15 %C Virtual Event %B Automated Deduction - CADE 28 %E Platzer, Andr&#233;; Sutcliffe, Geof %P 344 - 360 %I Springer %@ 978-3-030-79875-8 %B Lecture Notes in Artificial Intelligence %N 12699

%0 Journal Article %A England, Matthew %A Koepf, Wolfram %A Sadykov, Timor %A Seiler, Werner M. %A Sturm, Thomas %+ External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Foreword, with a Dedication to Andreas Weber : %G eng %U http://hdl.handle.net/21.11116/0000-0007-79E1-3 %R 10.1007/s11786-020-00476-y %7 2020 %D 2021 %J Mathematics in Computer Science %V 15 %& 173 %P 173 - 175 %I Springer %C New York, NY %@ false %U https://rdcu.be/cbpdy

%0 Journal Article %A England, Matthew %A Boulier, Fran&#231;ois %A Sadykov, Timor %A Sturm, Thomas %+ External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Foreword, with a Dedication to Vladimir Gerdt : %G eng %U http://hdl.handle.net/21.11116/0000-0009-4B06-D %R 10.1007/s11786-021-00509-0 %7 2021 %D 2021 %J Mathematics in Computer Science %V 15 %& 369 %P 369 - 371 %I Springer %C New York, NY %@ false %U https://rdcu.be/cyLbU

%0 Conference Proceedings %A Frohn, Florian %A Hark, Marcel %A Giesl, J&#252;rgen %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Termination of Polynomial Loops : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7FE3-B %R 10.1007/978-3-030-65474-0_5 %D 2021 %B 27th International Static Analysis Symposium %Z date of event: 2020-11-18 - 2020-11-20 %C Chicago, IL, USA (Online Event) %B Static Analysis %E Pichardie, David; Sighireanu, Mihaela %P 89 - 112 %I Springer %@ 978-3-030-65473-3 %B Lecture Notes in Computer Science %N 12389

%0 Journal Article %A Grigoriev, Dima %A Iosif, Alexandru %A Rahkooy, Hamid %A Sturm, Thomas %A Weber, Andreas %+ External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Efficiently and Effectively Recognizing Toricity of Steady State Varieties : %G eng %U http://hdl.handle.net/21.11116/0000-0007-79D1-5 %R 10.1007/s11786-020-00479-9 %7 2020 %D 2021 %J Mathematics in Computer Science %V 15 %& 199 %P 199 - 232 %I Springer %C New York, NY %@ false %U https://rdcu.be/cbpcc

%0 Journal Article %A Grigoriev, Dima %A Iosif, Alexandru %A Rahkooy, Hamid %A Sturm, Thomas %A Weber, Andreas %+ External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Efficiently and Effectively Recognizing Toricity of Steady State Varieties : %G eng %U http://hdl.handle.net/21.11116/0000-0009-4AD0-9 %R 10.1007/s11786-020-00479-9 %7 2021 %D 2021 %J Mathematics in Computer Science %V 15 %& 199 %P 199 - 232 %I Springer %C New York, NY

%0 Conference Proceedings %A Haifani, Fajar %A Tourret, Sophie %A Weidenbach, Christoph %+ 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 Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance : %G eng %U http://hdl.handle.net/21.11116/0000-0009-3F8D-3 %R 10.1007/978-3-030-79876-5_19 %D 2021 %B 28th International Conference on Automated Deduction %Z date of event: 2021-07-12 - 2021-07-15 %C Virtual Event %B Automated Deduction - CADE 28 %E Platzer, Andr&#233;; Sutcliffe, Geof %P 327 - 343 %I Springer %@ 978-3-030-79875-8 %B Lecture Notes in Artificial Intelligence %N 12699

%0 Conference Proceedings %A Haifani, Fajar %A Koopmann, Patrick %A Tourret, Sophie %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Abduction in EL via Translation to FOL : %G eng %U http://hdl.handle.net/21.11116/0000-000C-2152-2 %D 2021 %B Second Workshop on Second-Order Quantifier Elimination and Related Topics %Z date of event: 2021-11-04 - 2021-11-04 %C Online Event %B Second-Order Quantifier Elimination and Related Topics %E Schmidt, Renate A.; Wernhard, Christoph; Zhao, Yizheng %P 46 - 58 %I CEUR-WS %B CEUR Workshop Proceedings %N 3009 %@ false

%0 Journal Article %A Kruff, Niclas %A L&#252;ders, Christoph %A Radulescu, Ovidiu %A Sturm, Thomas %A Walcher, Sebastian %+ External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Algorithmic Reduction of Biological Networks With Multiple Time Scales : %G eng %U http://hdl.handle.net/21.11116/0000-0009-4B0A-9 %R 10.1007/s11786-021-00515-2 %7 2021 %D 2021 %J Mathematics in Computer Science %V 15 %& 499 %P 499 - 534 %I Springer %C New York,NY

%0 Conference Proceedings %A Nummelin, Visa %A Bentkamp, Alexander %A Tourret, Sophie %A Vukmirovi&#263;, Petar %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Superposition with First-class Booleans and Inprocessing Clausification : %G eng %U http://hdl.handle.net/21.11116/0000-0009-3F95-9 %R 10.1007/978-3-030-79876-5_22 %D 2021 %B 28th International Conference on Automated Deduction %Z date of event: 2021-07-12 - 2021-07-15 %C Virtual Event %B Automated Deduction - CADE 28 %E Platzer, Andr&#233;; Sutcliffe, Geof %P 378 - 395 %I Springer %@ 978-3-030-79875-8 %B Lecture Notes in Artificial Intelligence %N 12699

%0 Conference Proceedings %A Rahkooy, Hamid %A Vargas Montero, Cristian %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T A Graph Theoretical Approach for Testing Binomiality of Reversible Chemical Reaction Networks : %G eng %U http://hdl.handle.net/21.11116/0000-0009-479F-5 %R 10.1109/SYNASC51798.2020.00027 %D 2021 %B 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing %Z date of event: 2020-09-01 - 2020-09-04 %C Timisoara, Romania %B SYNASC 2020 %P 101 - 108 %I IEEE %@ 978-1-7281-7628-4

%0 Conference Proceedings %A Rahkooy, Hamid %A Sturm, Thomas %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Parametric Toricity of Steady State Varieties of Reaction Networks : %U http://hdl.handle.net/21.11116/0000-0009-4B0D-6 %R 10.1007/978-3-030-85165-1_18 %D 2021 %B 23rd International Workshop on Computer Algebra in Scienti&#64257;c Computing %Z date of event: 2021-09-13 - 2021-09-17 %C Sochi, Russia %B Computer Algebra in Scientific Computing %E Boulier, Fran&#231;ois; England, Matthew; Sadykov, Timur M.; Vorozhtsov, Evgenii v. %P 314 - 333 %I Springer %@ 978-3-030-85164-4 %B Lecture Notes in Computer Science %N 12865

%0 Report %A Rahkooy, Hamid %A Sturm, Thomas %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Parametric Toricity of Steady State Varieties of Reaction Networks : %G eng %U http://hdl.handle.net/21.11116/0000-0009-4B11-0 %U https://arxiv.org/abs/2105.10853 %D 2021 %X We study real steady state varieties of the dynamics of chemical reaction<br>networks. The dynamics are derived using mass action kinetics with parametric<br>reaction rates. The models studied are not inherently parametric in nature.<br>Rather, our interest in parameters is motivated by parameter uncertainty, as<br>reaction rates are typically either measured with limited precision or<br>estimated. We aim at detecting toricity and shifted toricity, using a framework<br>that has been recently introduced and studied for the non-parametric case over<br>both the real and the complex numbers. While toricity requires that the variety<br>specifies a subgroup of the direct power of the multiplicative group of the<br>underlying field, shifted toricity requires only a coset. In the non-parametric<br>case these requirements establish real decision problems. In the presence of<br>parameters we must go further and derive necessary and sufficient conditions in<br>the parameters for toricity or shifted toricity to hold. Technically, we use<br>real quantifier elimination methods. Our computations on biological networks<br>here once more confirm shifted toricity as a relevant concept, while toricity<br>holds only for degenerate parameter choices.<br> %K Quantitative Biology, Molecular Networks, q-bio.MN,Computer Science, Logic in Computer Science, cs.LO,Computer Science, Symbolic Computation, cs.SC,

%0 Report %A Rahkooy, Hamid %A Sturm, Thomas %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gr&#246;bner Systems : %G eng %U http://hdl.handle.net/21.11116/0000-0009-4B14-D %U https://arxiv.org/abs/2107.01706 %D 2021 %X We consider the problem of binomiality of the steady state ideals of<br>biochemical reaction networks. We are interested in finding polynomial<br>conditions on the parameters such that the steady state ideal of a chemical<br>reaction network is binomial under every specialisation of the parameters if<br>the conditions on the parameters hold. We approach the binomiality problem<br>using Comprehensive Gr\"obner systems. Considering rate constants as<br>parameters, we compute comprehensive Gr\"obner systems for various reactions.<br>In particular, we make automatic computations on n-site phosphorylations and<br>biomodels from the Biomodels repository using the grobcov library of the<br>computer algebra system Singular.<br> %K Quantitative Biology, Molecular Networks, q-bio.MN,Computer Science, Symbolic Computation, cs.SC

%0 Conference Proceedings %A Rahkooy, Hamid %A Sturm, Thomas %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gr&#246;bner Systems : %U http://hdl.handle.net/21.11116/0000-0009-4B0F-4 %R 10.1007/978-3-030-85165-1_19 %D 2021 %B 23rd International Workshop on Computer Algebra in Scienti&#64257;c Computing %Z date of event: 2021-09-13 - 2021-09-17 %C Sochi, Russia %B Computer Algebra in Scientific Computing %E Boulier, Fran&#231;ois; England, Matthew; Sadykov, Timur M.; Vorozhtsov, Evgenii v. %P 334 - 352 %I Springer %@ 978-3-030-85164-4 %B Lecture Notes in Computer Science %N 12865

%0 Conference Proceedings %A Schurr, Hans-J&#246;rg %A Fleury, Mathias %A Desharnais, Martin %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant : %G eng %U http://hdl.handle.net/21.11116/0000-0009-3F9B-3 %R 10.1007/978-3-030-79876-5_26 %D 2021 %B 28th International Conference on Automated Deduction %Z date of event: 2021-07-12 - 2021-07-15 %C Virtual Event %B Automated Deduction - CADE 28 %E Platzer, Andr&#233;; Sutcliffe, Geof %P 450 - 467 %I Springer %@ 978-3-030-79875-8 %B Lecture Notes in Artificial Intelligence %N 12699

%0 Journal Article %A Seiler, Werner M. %A Sei&#223;, Matthias %A Sturm, Thomas %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations : %G eng %U http://hdl.handle.net/21.11116/0000-0007-79D5-1 %R 10.1007/s11786-020-00485-x %7 2020 %D 2021 %J Mathematics in Computer Science %V 15 %& 333 %P 333 - 352 %I Springer %C New York, NY %@ false %U https://rdcu.be/cbpcP

%0 Journal Article %A Sutcliffe, Geoff %A Desharnais, Martin %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T The CADE-28 Automated Theorem Proving System Competition - CASC-28 : %G eng %U http://hdl.handle.net/21.11116/0000-000A-3869-2 %R 10.3233/AIC-210235 %7 2021 %D 2021 %J AI Communications %V 34 %N 4 %& 259 %P 259 - 276 %I IOS %C Amsterdam, Netherlands %@ false

%0 Conference Proceedings %A Tourret, Sophie %A Blanchette, Jasmin Christian %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T A Modular Isabelle Framework for Verifying Saturation Provers : %G eng %U http://hdl.handle.net/21.11116/0000-0008-0A0F-E %R 10.1145/3437992.3439912 %D 2021 %B 10th ACM SIGPLAN International Conference on Certified Programs and Proofs %Z date of event: 2021-01-17 - 2021-01-19 %C Virtual, Denmark %B CPP '21 %E Hri&#355;cu, C&#259;t&#259;lin; Popescu, Andrei %P 224 - 237 %I ACM %@ 978-1-4503-8299-1

%0 Journal Article %A Voigt, Marco %+ Automation of Logic, MPI for Informatics, Max Planck Society %T Decidable &#8707;&#8727;&#8704;&#8727; 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 2021 %J Journal of Automated Reasoning %V 65 %& 357 %P 357 - 423 %I Springer %C New York, NY %@ false

%0 Conference Proceedings %A Vukmirovi&#263;, Petar %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Cruanes, Simon %A Nummelin, Visa %A Tourret, Sophie %+ External Organizations External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Making Higher-Order Superposition Work : %G eng %U http://hdl.handle.net/21.11116/0000-0009-3FA2-A %R 10.1007/978-3-030-79876-5_24 %D 2021 %B 28th International Conference on Automated Deduction %Z date of event: 2021-07-12 - 2021-07-15 %C Virtual Event %B Automated Deduction - CADE 28 %E Platzer, Andr&#233;; Sutcliffe, Geof %P 415 - 432 %I Springer %@ 978-3-030-79875-8 %B Lecture Notes in Artificial Intelligence %N 12699

%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

%0 Report %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Cruanes, Simon %A Waldmann, Uwe %+ External Organizations External Organizations 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-0008-0A5F-4 %U https://arxiv.org/abs/2005.02094 %D 2020 %X We introduce refutationally complete superposition calculi for intentional<br>and extensional clausal $\lambda$-free higher-order logic, two formalisms that<br>allow partial application and applied variables. The calculi are parameterized<br>by a term order that need not be fully monotonic, making it possible to employ<br>the $\lambda$-free higher-order lexicographic path and Knuth-Bendix orders. We<br>implemented the calculi in the Zipperposition prover and evaluated them on<br>Isabelle/HOL and TPTP benchmarks. They appear promising as a stepping stone<br>towards complete, highly efficient automatic theorem provers for full<br>higher-order logic.<br> %K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Artificial Intelligence, cs.AI

%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

%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&#353;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

%0 Report %A Bromberger, Martin %A Fiori, Alberto %A Weidenbach, Christoph %+ 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 SCL with Theory Constraints : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7AFE-3 %U https://arxiv.org/abs/2003.04627 %D 2020 %X We lift the SCL calculus for first-order logic without equality to the SCL(T)<br>calculus for first-order logic without equality modulo a background theory. In<br>a nutshell, the SCL(T) calculus describes a new way to guide hierarchic<br>resolution inferences by a partial model assumption instead of an a priori<br>fixed order as done for instance in hierarchic superposition. The model<br>representation consists of ground background theory literals and ground<br>foreground first-order literals. One major advantage of the model guided<br>approach is that clauses generated by SCL(T) enjoy a non-redundancy property<br>that makes expensive testing for tautologies and forward subsumption completely<br>obsolete. SCL(T) is a semi-decision procedure for pure clause sets that are<br>clause sets without first-order function symbols ranging into the background<br>theory sorts. Moreover, SCL(T) can be turned into a decision procedure if the<br>considered combination of a first-order logic modulo a background theory enjoys<br>an abstract finite model property.<br> %K Computer Science, Logic in Computer Science, cs.LO

%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

%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

%0 Conference Proceedings %A Faqeh, Rasha %A Fetzer, Christof %A Hermanns, Holger %A Hoffmann, J&#246;rg %A Klauck, Michaela %A K&#246;hl, Maximilian A. %A Steinmetz, Marcel %A Weidenbach, Christoph %+ External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7B0E-1 %R 10.1007/978-3-030-61470-6_25 %D 2020 %B 9th International Symposium on Leveraging Applications of Formal Methods, Veri&#64257;cation and Validation %Z date of event: 2020-10-20 - 2020-10-30 %C Rhodes, Greece (Virtual Event) %B Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles %E Margaria, Tiziana; Steffen, Bernhard %P 416 - 439 %I Springer %@ 978-3-030-61469-0 %B Lecture Notes in Computer Science %N 12477

%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 %U urn:nbn:de:bsz:291--ds-301796 %F OTHER: hdl:20.500.11880/28722 %I Universit&#228;t des Saarlandes %C Saarbr&#252;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

%0 Conference Proceedings %A Fleury, Mathias %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T A Verified SAT Solver Framework including Optimization and Partial Valuations : %G eng %U http://hdl.handle.net/21.11116/0000-0007-78C7-2 %R 10.29007/96wb %D 2020 %B 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning %Z date of event: 2021-01-12 - 2021-01-13 %C Virtual Conferernce %B LPAR-23 %E Albert, Elvira; Kov&#225;cs, Laura %P 212 - 229 %I EasyChair %B EasyChair Proceedings in Computing %N 73 %@ false %U https://easychair.org/publications/paper/b7Cr

%0 Report %A Frohn, Florian %+ Automation of Logic, MPI for Informatics, Max Planck Society %T A Calculus for Modular Loop Acceleration : %G eng %U http://hdl.handle.net/21.11116/0000-0007-CEFC-6 %U https://arxiv.org/abs/2001.01516 %D 2020 %X Loop acceleration can be used to prove safety, reachability, runtime bounds,<br>and (non-)termination of programs operating on integers. To this end, a variety<br>of acceleration techniques has been proposed. However, all of them are<br>monolithic: Either they accelerate a loop successfully or they fail completely.<br>In contrast, we present a calculus that allows for combining acceleration<br>techniques in a modular way and we show how to integrate many existing<br>acceleration techniques into our calculus. Moreover, we propose two novel<br>acceleration techniques that can be incorporated into our calculus seamlessly.<br>An empirical evaluation demonstrates the applicability of our approach.<br> %K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Programming Languages, cs.PL

%0 Journal Article %A Frohn, Florian %A Naaf, Matthias %A Brockschmidt, Marc %A Giesl, J&#252;rgen %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations %T Inferring Lower Runtime Bounds for Integer Programs : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7FCD-5 %R 10.1145/3410331 %7 2020 %D 2020 %J ACM Transactions on Programming Languages and Systems %V 42 %Z sequence number: 13 %I ACM %C New York, NY %@ false

%0 Conference Proceedings %A Frohn, Florian %+ Automation of Logic, MPI for Informatics, Max Planck Society %T A Calculus for Modular Loop Acceleration : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7FCF-3 %R 10.1007/978-3-030-45190-5_4 %D 2020 %B 26th International Conference on Tools and Algorithms for the Construction and Analysis of System %Z date of event: 2020-04-25 - 2020-04-30 %C Dublin, Ireland (Online Event) %B Tools and Algorithms for the Construction and Analysis of Systems %E Biere, Armin; Parker, David %P 58 - 76 %I Springer %@ 978-3-030-45189-9 %B Lecture Notes in Computer Science %N 12078

%0 Conference Proceedings %A Haifani, Fajar %A Koopmann, Patrick %A Tourret, Sophie %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T On a Notion of Relevance : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7968-D %U http://ceur-ws.org/Vol-2663/paper-10.pdf %D 2020 %B 33rd International Workshop on Description Logics %Z date of event: 2020-09-12 - 2020-09-14 %C Rhodes, Greece (Virtual Event) %B Proceedings of the 33rd International Workshop on Description Logics %E Borgwardt , Stefan; Meyer, Thomas %Z sequence number: 10 %I ceur-ws.org %B CEUR Workshop Proceedings %N 2663 %@ false

%0 Conference Proceedings %A Hark, Marcel %A Frohn, Florian %A Giesl, J&#252;rgen %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Polynomial Loops: Beyond Termination : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7FD4-C %R 10.29007/nxv1 %D 2020 %B 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning %Z date of event: 2021-01-12 - 2021-01-13 %C Virtual Conferernce %B LPAR-23 %E Albert, Elvira; Kov&#225;cs, Laura %P 279 - 297 %I EasyChair %B EasyChair Proceedings in Computing %N 73 %@ false %U https://easychair.org/publications/paper/Bl5n

%0 Conference Proceedings %A Koopmann, Patrick %A Del-Pinto, Warren %A Tourret, Sophie %A Schmidt, Renate A. %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Signature-Based Abduction for Expressive Description Logics : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7961-4 %R 10.24963/kr.2020/59 %D 2020 %B 17th International Conference on Principles of Knowledge Representation and Reasoning %Z date of event: 2020-09-12 - 2020-09-18 %C Rhodes, Greece (Virtual Conference) %B Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning %E Calvanese, Diego; Erdem, Esra; Thielscher, Michael %P 592 - 602 %I IJCAI Organization %@ 978-0-9992411-7-2 %U https://doi.org/10.24963/kr.2020/59

%0 Report %A Kruff, Niclas %A L&#252;ders, Christoph %A Radulescu, Ovidiu %A Sturm, Thomas %A Walcher, Sebastian %+ External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Algorithmic Reduction of Biological Networks With Multiple Time Scales : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7A12-C %U https://arxiv.org/abs/2010.10129 %D 2020 %X We present a symbolic algorithmic approach that allows to compute invariant<br>manifolds and corresponding reduced systems for differential equations modeling<br>biological networks which comprise chemical reaction networks for cellular<br>biochemistry, and compartmental models for pharmacology, epidemiology and<br>ecology. Multiple time scales of a given network are obtained by scaling, based<br>on tropical geometry. Our reduction is mathematically justified within a<br>singular perturbation setting using a recent result by Cardin and Teixeira. The<br>existence of invariant manifolds is subject to hyperbolicity conditions, which<br>we test algorithmically using Hurwitz criteria. We finally obtain a sequence of<br>nested invariant manifolds and respective reduced systems on those manifolds.<br>Our theoretical results are generally accompanied by rigorous algorithmic<br>descriptions suitable for direct implementation based on existing off-the-shelf<br>software systems, specifically symbolic computation libraries and<br>Satisfiability Modulo Theories solvers. We present computational examples taken<br>from the well-known BioModels database using our own prototypical<br>implementations.<br> %K Quantitative Biology, Molecular Networks, q-bio.MN,Computer Science, Logic in Computer Science, cs.LO,Computer Science, Symbolic Computation, cs.SC,Mathematics, Dynamical Systems, math.DS,

%0 Conference Proceedings %A Rahkooy, Hamid %A Radulescu, Ovidiu %A Sturm, Thomas %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T A Linear Algebra Approach for Detecting Binomiality of Steady State Ideals of Reversible Chemical Reaction Networks : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7A1C-2 %R 10.1007/978-3-030-60026-6_29 %D 2020 %B 22nd International Workshop on Computer Algebra in Scientific Computing %Z date of event: 2020-09-14 - 2020-09-18 %C Linz, Austria (Virtual Event) %B Computer Algebra in Scientific Computing %E Boulier, Fran&#231;ois; England, Matthew; Sadykov, Timur M.; Vorozhtsov, Evgenii V. %P 492 - 509 %I Springer %B Lecture Notes in Computer Science %N 12291

%0 Report %A Rahkooy, Hamid %A Vargas Montero, Cristian %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T A Graph Theoretical Approach for Testing Binomiality of Reversible Chemical Reaction Networks : %G eng %U http://hdl.handle.net/21.11116/0000-0007-B427-2 %U https://arxiv.org/abs/2010.12615 %D 2020 %X We study binomiality of the steady state ideals of chemical reaction<br>networks. Considering rate constants as indeterminates, the concept of<br>unconditional binomiality has been introduced and an algorithm based on linear<br>algebra has been proposed in a recent work for reversible chemical reaction<br>networks, which has a polynomial time complexity upper bound on the number of<br>species and reactions. In this article, using a modified version of<br>species--reaction graphs, we present an algorithm based on graph theory which<br>performs by adding and deleting edges and changing the labels of the edges in<br>order to test unconditional binomiality. We have implemented our graph<br>theoretical algorithm as well as the linear algebra one in Maple and made<br>experiments on biochemical models. Our experiments show that the performance of<br>the graph theoretical approach is similar to or better than the linear algebra<br>approach, while it is drastically faster than Groebner basis and quantifier<br>elimination methods.<br> %K Computer Science, Symbolic Computation, cs.SC,Mathematics, Commutative Algebra, math.AC

%0 Conference Proceedings %A Rahkooy, Hamid %A Sturm, Thomas %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T First-Order Tests for Toricity : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7A18-6 %R 10.1007/978-3-030-60026-6_30 %D 2020 %B 22nd International Workshop on Computer Algebra in Scientific Computing %Z date of event: 2020-09-14 - 2020-09-18 %C Linz, Austria (Virtual Event) %B Computer Algebra in Scientific Computing %E Boulier, Fran&#231;ois; England, Matthew; Sadykov, Timur M.; Vorozhtsov, Evgenii V. %P 510 - 527 %I Springer %B Lecture Notes in Computer Science %N 12291

%0 Report %A Rahkooy, Hamid %A Sturm, Thomas %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T First-Order Tests for Toricity : %G eng %U http://hdl.handle.net/21.11116/0000-0008-0A76-9 %U https://arxiv.org/abs/2002.03586 %D 2020 %X Motivated by problems arising with the symbolic analysis of steady state<br>ideals in Chemical Reaction Network Theory, we consider the problem of testing<br>whether the points in a complex or real variety with non-zero coordinates form<br>a coset of a multiplicative group. That property corresponds to Shifted<br>Toricity, a recent generalization of toricity of the corresponding polynomial<br>ideal. The key idea is to take a geometric view on varieties rather than an<br>algebraic view on ideals. Recently, corresponding coset tests have been<br>proposed for complex and for real varieties. The former combine numerous<br>techniques from commutative algorithmic algebra with Gr\"obner bases as the<br>central algorithmic tool. The latter are based on interpreted first-order logic<br>in real closed fields with real quantifier elimination techniques on the<br>algorithmic side. Here we take a new logic approach to both theories, complex<br>and real, and beyond. Besides alternative algorithms, our approach provides a<br>unified view on theories of fields and helps to understand the relevance and<br>interconnection of the rich existing literature in the area, which has been<br>focusing on complex numbers, while from a scientific point of view the<br>(positive) real numbers are clearly the relevant domain in chemical reaction<br>network theory. We apply prototypical implementations of our new approach to a<br>set of 129 models from the BioModels repository.<br> %K Computer Science, Symbolic Computation, cs.SC,Quantitative Biology, Molecular Networks, q-bio.MN

%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 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 %V 64 %& 1169 %P 1169 - 1195 %I D. Reidel Pub. Co. %C Dordrecht, Holland %@ false

%0 Report %A Seiler, Werner M. %A Seiss, Matthias %A Sturm, Thomas %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7A09-7 %U https://arxiv.org/abs/2003.00740 %D 2020 %X We discuss the effective computation of geometric singularities of implicit<br>ordinary differential equations over the real numbers using methods from logic.<br>Via the Vessiot theory of differential equations, geometric singularities can<br>be characterised as points where the behaviour of a certain linear system of<br>equations changes. These points can be discovered using a specifically adapted<br>parametric generalisation of Gaussian elimination combined with heuristic<br>simplification techniques and real quantifier elimination methods. We<br>demonstrate the relevance and applicability of our approach with computational<br>experiments using a prototypical implementation in Reduce.<br> %K Mathematics, Logic, math.LO,Mathematics, Commutative Algebra, math.AC,Mathematics, Differential Geometry, math.DG,

%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

%0 Conference Proceedings %A Waldmann, Uwe %A Tourret, Sophie %A Robillard, Simon %A Blanchette, Jasmin Christian %+ 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 Comprehensive Framework for Saturation Theorem Proving : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7971-2 %R 10.1007/978-3-030-51074-9_18 %D 2020 %B 10th International Joint Conference on Automated Reasoning %Z date of event: 2020-07-01 - 2020-07-04 %C Paris, France (Virtual Conference) %B Automated Reasoning %E Peltier, Nicolas; Sofronie-Stokkermans, Viorica %P 316 - 334 %I Springer %@ 978-3-030-51073-2 %B Lecture Notes in Artificial Intelligence %N 12166

%0 Book Section %A Baumgartner, Peter %A Waldmann, Uwe %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Hierarchic Superposition Revisited : %G eng %U http://hdl.handle.net/21.11116/0000-0004-03B5-C %R 10.1007/978-3-030-22102-7_2 %D 2019 %B Description Logic, Theory Combination, and All That %E Lutz, Carsten; Sattler, Uli; Tinelli, Cesare; Turhan, Anni-Yasmin; Wolter, Frank; Baader, Franz %P 15 - 56 %I Springer %C Berlin %@ 978-3-030-22101-0 %S Lecture Notes in Computer Science %N 11560

%0 Report %A Baumgartner, Peter %A Waldmann, Uwe %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Hierarchic Superposition Revisited : %G eng %U http://hdl.handle.net/21.11116/0000-0004-03C0-F %U http://arxiv.org/abs/1904.03776 %D 2019 %X Many applications of automated deduction require reasoning in first-order<br>logic modulo background theories, in particular some form of integer<br>arithmetic. A major unsolved research challenge is to design theorem provers<br>that are "reasonably complete" even in the presence of free function symbols<br>ranging into a background theory sort. The hierarchic superposition calculus of<br>Bachmair, Ganzinger, and Waldmann already supports such symbols, but, as we<br>demonstrate, not optimally. This paper aims to rectify the situation by<br>introducing a novel form of clause abstraction, a core component in the<br>hierarchic superposition calculus for transforming clauses into a form needed<br>for internal operation. We argue for the benefits of the resulting calculus and<br>provide two new completeness results: one for the fragment where all<br>background-sorted terms are ground and another one for a special case of linear<br>(integer or rational) arithmetic as a background theory.<br> %K Computer Science, Logic in Computer Science, cs.LO

%0 Journal Article %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Klakow, Dietrich %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T A Formal Proof of the Expressiveness of Deep Learning : %G eng %U http://hdl.handle.net/21.11116/0000-0004-7A8F-3 %R 10.1007/s10817-018-9481-5 %7 2019 %D 2019 %J Journal of Automated Reasoning %V 63 %N 2 %& 347 %P 347 - 368 %I Springer %C New York, NY %@ false

%0 Conference Proceedings %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Tourret, Sophie %A Vukmirovi&#263;, Petar %A Waldmann, Uwe %+ External Organizations 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 Superposition with Lambdas : %G eng %U http://hdl.handle.net/21.11116/0000-0005-885C-B %R 10.1007/978-3-030-29436-6_4 %D 2019 %B 27th International Conference on Automated Deduction %Z date of event: 2019-08-27 - 2019-08-30 %C Natal, Brazil %B Automated Deduction -- CADE 27 %E Fontaine, Pascal %P 55 - 73 %I Springer %@ 978-3-030-29435-9 %B Lecture Notes in Artificial Intelligence %N 11716 %@ false

%0 Journal Article %A Blanchette, Jasmin Christian %A Gheri, Lorenzo %A Popescu, Andrei %A Traytel, Dmitriy %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations %T Bindings as Bounded Natural Functors : %G eng %U http://hdl.handle.net/21.11116/0000-0002-E59A-E %R 10.1145/3290335 %7 2019 %D 2019 %J Proceedings of the ACM on Programming Languages %O PACMPL %V 3 %Z sequence number: 22 %I ACM %C New York, NY %@ false %B 46th ACM SIGPLAN Symposium on Principles of Programming Languages %O POPL 2019 Sun 13 - Sat 19 January 2019 Cascais, Portugal

%0 Conference Proceedings %A Blanchette, Jasmin Christian %+ Automation of Logic, MPI for Informatics, Max Planck Society %T Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk) : %G eng %U http://hdl.handle.net/21.11116/0000-0002-E5A0-6 %R 10.1145/3293880.3294087 %D 2019 %B 8th ACM SIGPLAN International Conference on Certified Programs and Proofs %Z date of event: 2019-01-14 - 2019-01-15 %C Cascais, Portugal %B CPP'19 %E Mahboubi, Assia; Myreen, Magnus O. %P 1 - 13 %I ACM %@ 978-1-4503-6222-1

%0 Report %A Bradford, Russell %A Davenport, James H. %A England, Matthew %A Errami, Hassan %A Gerdt, Vladimir %A Grigoriev, Dima %A Hoyt, Charles %A Ko&#353;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-FF3C-D %U http://arxiv.org/abs/1902.04882 %D 2019 %X We consider a problem from biological network analysis of determining regions<br>in a parameter space over which there are multiple steady states for positive<br>real values of variables and parameters. We describe multiple approaches to<br>address the problem using tools from Symbolic Computation. We describe how<br>progress was made to achieve semi-algebraic descriptions of the<br>multistationarity regions of parameter space, and compare symbolic results to<br>numerical methods. The biological networks studied are models of the<br>mitogen-activated protein kinases (MAPK) network which has already consumed<br>considerable effort using special insights into its structure of corresponding<br>models. Our main example is a model with 11 equations in 11 variables and 19<br>parameters, 3 of which are of interest for symbolic treatment. The model also<br>imposes positivity conditions on all variables and parameters.<br> We apply combinations of symbolic computation methods designed for mixed<br>equality/inequality systems, specifically virtual substitution, lazy real<br>triangularization and cylindrical algebraic decomposition, as well as a<br>simplification technique adapted from Gaussian elimination and graph theory. We<br>are able to determine multistationarity of our main example over a<br>2-dimensional parameter space. We also study a second MAPK model and a symbolic<br>grid sampling technique which can locate such regions in 3-dimensional<br>parameter space.<br> %K Computer Science, Symbolic Computation, cs.SC

%0 Thesis %A Bromberger, Martin %Y Weidenbach, Christoph %A referee: Sturm, Thomas %+ 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 Automation of Logic, MPI for Informatics, Max Planck Society %T Decision Procedures for Linear Arithmetic : %G eng %U http://hdl.handle.net/21.11116/0000-0007-713E-5 %R 10.22028/D291-30636 %U urn:nbn:de:bsz:291--ds-306363 %F OTHER: hdl:20.500.11880/28955 %I Universit&#228;t des Saarlandes %C Saarbr&#252;cken %D 2019 %P 341 p. %V phd %9 phd %U https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28955

%0 Conference Proceedings %A Bromberger, Martin %A Fleury, Mathias %A Schwarz, Simon %A Weidenbach, Christoph %+ 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 SPASS-SATT: A CDCL(LA) Solver : %G eng %U http://hdl.handle.net/21.11116/0000-0005-8846-3 %R 10.1007/978-3-030-29436-6_7 %D 2019 %B 27th International Conference on Automated Deduction %Z date of event: 2019-08-27 - 2019-08-30 %C Natal, Brazil %B Automated Deduction -- CADE 27 %E Fontaine, Pascal %P 111 - 122 %I Springer %@ 978-3-030-29435-9 %B Lecture Notes in Artificial Intelligence %N 11716 %@ false

%0 Journal Article %A Cropper, Andrew %A Tourret, Sophie %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Logical Reduction of Metarules : %G eng %U http://hdl.handle.net/21.11116/0000-0005-8859-E %R 10.1007/s10994-019-05834-x %7 2019 %D 2019 %J Machine Learning %V 109 %& 1323 %P 1323 - 1369 %I Springer %C Dordrecht %@ false %B Special Issue of the Inductive Logic Programming (ILP) 2019 %O ILP 2019 The 29th International Conference on Inductive Logic Programming. 3-5 Sep 2019, Plovdiv, Bulgaria

%0 Conference Proceedings %A Fiori, Alberto %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T SCL Clause Learning from Simple Models : %G eng %U http://hdl.handle.net/21.11116/0000-0005-883F-C %R 10.1007/978-3-030-29436-6_14 %D 2019 %B 27th International Conference on Automated Deduction %Z date of event: 2019-08-27 - 2019-08-30 %C Natal, Brazil %B Automated Deduction -- CADE 27 %E Fontaine, Pascal %P 233 - 249 %I Springer %@ 978-3-030-29435-9 %B Lecture Notes in Artificial Intelligence %N 11716 %@ false

%0 Journal Article %A Fleury, Mathias %A Schurr, Hans-J&#246;rg %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Reconstructing veriT Proofs in Isabelle/HOL : %G eng %U http://hdl.handle.net/21.11116/0000-0005-8879-A %R 10.4204/EPTCS.301.6 %U http://arxiv.org/abs/1908.09480 %7 2019 %D 2019 %X Automated theorem provers are now commonly used within interactive theorem<br>provers to discharge an increasingly large number of proof obligations. To<br>maintain the trustworthiness of a proof, the automatically found proof must be<br>verified inside the proof assistant. We present here a reconstruction procedure<br>in the proof assistant Isabelle/HOL for proofs generated by the satisfiability<br>modulo theories solver veriT which is part of the smt tactic. We describe in<br>detail the architecture of our improved reconstruction method and the<br>challenges we faced in designing it. Our experiments show that the<br>veriT-powered smt tactic is regularly suggested by Sledgehammer as the fastest<br>method to automatically solve proof goals.<br> %K Computer Science, Logic in Computer Science, cs.LO %J Electronic Proceedings in Theoretical Computer Science %O EPTCS %N 301 %& 36 %P 36 - 50 %B Proceedings Sixth Workshop on Proof eXchange for Theorem Proving %O PxTP 2019 Natal, Brazil, August 26, 2019

%0 Conference Proceedings %A Fleury, Mathias %+ Automation of Logic, MPI for Informatics, Max Planck Society %T Optimizing a Verified SAT Solver : %G eng %U http://hdl.handle.net/21.11116/0000-0004-86AA-5 %R 10.1007/978-3-030-20652-9_10 %D 2019 %B 1th NASA Formal Methods Symposium %Z date of event: 2019-05-07 - 2019-05-09 %C Houston, TX, USA %B NASA Formal Methods %E Badger, Julia M.; Rozier, Kristin Yvonne %P 148 - 165 %I Springer %@ 978-3-030-20651-2 %B Lecture Notes in Computer Science %N 11460

%0 Report %A Frohn, Florian %A Naaf, Matthias %A Brockschmidt, Marc %A Giesl, J&#252;rgen %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations %T Inferring Lower Runtime Bounds for Integer Programs : %G eng %U http://hdl.handle.net/21.11116/0000-0007-CEF3-F %U https://arxiv.org/abs/1911.01077 %D 2019 %X We present a technique to infer lower bounds on the worst-case runtime<br>complexity of integer programs, where in contrast to earlier work, our approach<br>is not restricted to tail-recursion. Our technique constructs symbolic<br>representations of program executions using a framework for iterative,<br>under-approximating program simplification. The core of this simplification is<br>a method for (under-approximating) program acceleration based on recurrence<br>solving and a variation of ranking functions. Afterwards, we deduce asymptotic<br>lower bounds from the resulting simplified programs using a special-purpose<br>calculus and an SMT encoding. We implemented our technique in our tool LoAT and<br>show that it infers non-trivial lower bounds for a large class of examples.<br> %K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Programming Languages, cs.PL

%0 Report %A Frohn, Florian %A Giesl, J&#252;rgen %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Proving Non-Termination via Loop Acceleration : %G eng %U http://hdl.handle.net/21.11116/0000-0007-CEE0-4 %U https://arxiv.org/abs/1905.11187 %D 2019 %X We present the first approach to prove non-termination of integer programs<br>that is based on loop acceleration. If our technique cannot show<br>non-termination of a loop, it tries to accelerate it instead in order to find<br>paths to other non-terminating loops automatically. The prerequisites for our<br>novel loop acceleration technique generalize a simple yet effective<br>non-termination criterion. Thus, we can use the same program transformations to<br>facilitate both non-termination proving and loop acceleration. In particular,<br>we present a novel invariant inference technique that is tailored to our<br>approach. An extensive evaluation of our fully automated tool LoAT shows that<br>it is competitive with the state of the art.<br> %K Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A Frohn, Florian %A Giesl, J&#252;rgen %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Termination of Triangular Integer Loops is Decidable : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7E8E-D %R 10.1007/978-3-030-25543-5_24 %D 2019 %B 31st International Conference on Computer-Aided Verification %Z date of event: 2019-07-15 - 2019-07-18 %C York City, NY, USA %B Computer Aided Verification %E Dillig, Isil; Tasiran, Serdar %P 426 - 444 %I Springer %@ 978-3-030-25543-5 %B Lecture Notes in Computer Science %N 11562

%0 Conference Proceedings %A Frohn, Florian %A Giesl, J&#252;rgen %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Proving Non-Termination via Loop Acceleration : %G eng %U http://hdl.handle.net/21.11116/0000-0007-7EDD-4 %R 10.23919/FMCAD.2019.8894271 %D 2019 %B 19th International Conference on Formal Methods in Computer Aided Design %Z date of event: 2019-10-22 - 2019-10-25 %C San Jose, CA, USA %B Formal Methods in Computer Aided Design %P 221 - 230 %I IEEE %@ 978-0-9835678-9-9

%0 Report %A Frohn, Florian %A Hark, Marcel %A Giesl, J&#252;rgen %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T On the Decidability of Termination for Polynomial Loops : %G eng %U http://hdl.handle.net/21.11116/0000-0007-CEE8-C %U https://arxiv.org/abs/1910.11588 %D 2019 %X We consider the termination problem for triangular weakly non-linear loops<br>(twn-loops) over some ring $\mathcal{S}$ like $\mathbb{Z}$, $\mathbb{Q}$, or<br>$\mathbb{R}$. Essentially, the guard of such a loop is an arbitrary Boolean<br>formula over (possibly non-linear) polynomial inequations, and the body is a<br>single assignment $(x_1, \ldots, x_d) \longleftarrow (c_1 \cdot x_1 + p_1,<br>\ldots, c_d \cdot x_d + p_d)$ where each $x_i$ is a variable, $c_i \in<br>\mathcal{S}$, and each $p_i$ is a (possibly non-linear) polynomial over<br>$\mathcal{S}$ and the variables $x_{i+1},\ldots,x_{d}$. We present a reduction<br>from the question of termination to the existential fragment of the first-order<br>theory of $\mathcal{S}$ and $\mathbb{R}$. For loops over $\mathbb{R}$, our<br>reduction entails decidability of termination. For loops over $\mathbb{Z}$ and<br>$\mathbb{Q}$, it proves semi-decidability of non-termination.<br> Furthermore, we present a transformation to convert certain non-twn-loops<br>into twn-form. Then the original loop terminates iff the transformed loop<br>terminates over a specific subset of $\mathbb{R}$, which can also be checked<br>via our reduction. This transformation also allows us to prove tight complexity<br>bounds for the termination problem for two important classes of loops which can<br>always be transformed into twn-loops.<br> %K Computer Science, Logic in Computer Science, cs.LO

%0 Report %A Frohn, Florian %A Giesl, J&#252;rgen %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Termination of Triangular Integer Loops is Decidable : %G eng %U http://hdl.handle.net/21.11116/0000-0007-CED1-5 %U https://arxiv.org/abs/1905.08664 %D 2019 %X We consider the problem whether termination of affine integer loops is<br>decidable. Since Tiwari conjectured decidability in 2004, only special cases<br>have been solved. We complement this work by proving decidability for the case<br>that the update matrix is triangular.<br> %K Computer Science, Logic in Computer Science, cs.LO

%0 Report %A Grigoriev, Dima %A Iosif, Alexandru %A Rahkooy, Hamid %A Sturm, Thomas %A Weber, Andreas %+ External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Efficiently and Effectively Recognizing Toricity of Steady State Varieties : %G eng %U http://hdl.handle.net/21.11116/0000-0005-890F-1 %U http://arxiv.org/abs/1910.04100 %D 2019 %X We consider the problem of testing whether the points in a complex or real<br>variety with non-zero coordinates form a multiplicative group or, more<br>generally, a coset of a multiplicative group. For the coset case, we study the<br>notion of shifted toric varieties which generalizes the notion of toric<br>varieties. This requires a geometric view on the varieties rather than an<br>algebraic view on the ideals. We present algorithms and computations on 129<br>models from the BioModels repository testing for group and coset structures<br>over both the complex numbers and the real numbers. Our methods over the<br>complex numbers are based on Gr\"obner basis techniques and binomiality tests.<br>Over the real numbers we use first-order characterizations and employ real<br>quantifier elimination. In combination with suitable prime decompositions and<br>restrictions to subspaces it turns out that almost all models show coset<br>structure. Beyond our practical computations, we give upper bounds on the<br>asymptotic worst-case complexity of the corresponding problems by proposing<br>single exponential algorithms that test complex or real varieties for toricity<br>or shifted toricity. In the positive case, these algorithms produce generating<br>binomials. In addition, we propose an asymptotically fast algorithm for testing<br>membership in a binomial variety over the algebraic closure of the rational<br>numbers.<br> %K Quantitative Biology, Molecular Networks, q-bio.MN,Computer Science, Symbolic Computation, cs.SC,Mathematics, Algebraic Geometry, math.AG

%0 Conference Proceedings %A Schlichtkrull, Anders %A Blanchette, Jasmin Christian %A Traytel, Dmitriy %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T A Verified Prover Based on Ordered Resolution : %G eng %U http://hdl.handle.net/21.11116/0000-0002-E59E-A %R 10.1145/3293880.3294100 %D 2019 %B 8th ACM SIGPLAN International Conference on Certified Programs and Proofs %Z date of event: 2019-01-14 - 2019-01-15 %C Cascais, Portugal %B CPP'19 %E Mahboubi, Assia; Myreen, Magnus O. %P 152 - 165 %I ACM %@ 978-1-4503-6222-1

%0 Conference Proceedings %A Teucke, Andreas %A Voigt, Marco %A Weidenbach, Christoph %+ 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 On the Expressivity and Applicability of Model Representation Formalisms : %G eng %U http://hdl.handle.net/21.11116/0000-0005-883B-0 %R 10.1007/978-3-030-29007-8_2 %D 2019 %B 12th International Symposium on Frontiers of Combining Systems %Z date of event: 2019-09-04 - 2019-09-06 %C London, UK %B Frontiers of Combining Systems %E Herzig, Andreas; Popescu, Andrei %P 22 - 39 %I Springer %@ 978-3-030-29006-1 %B Lecture Notes in Artificial Intelligence %N 11715 %@ false

%0 Report %A Teucke, Andreas %A Voigt, Marco %A Weidenbach, Christoph %+ 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 On the Expressivity and Applicability of Model Representation Formalisms : %G eng %U http://hdl.handle.net/21.11116/0000-0004-031B-B %U http://arxiv.org/abs/1905.03651 %D 2019 %X A number of first-order calculi employ an explicit model representation<br>formalism for automated reasoning and for detecting satisfiability. Many of<br>these formalisms can represent infinite Herbrand models. The first-order<br>fragment of monadic, shallow, linear, Horn (MSLH) clauses, is such a formalism<br>used in the approximation refinement calculus. Our first result is a finite<br>model property for MSLH clause sets. Therefore, MSLH clause sets cannot<br>represent models of clause sets with inherently infinite models. Through a<br>translation to tree automata, we further show that this limitation also applies<br>to the linear fragments of implicit generalizations, which is the formalism<br>used in the model-evolution calculus, to atoms with disequality constraints,<br>the formalisms used in the non-redundant clause learning calculus (NRCL), and<br>to atoms with membership constraints, a formalism used for example in decision<br>procedures for algebraic data types. Although these formalisms cannot represent<br>models of clause sets with inherently infinite models, through an additional<br>approximation step they can. This is our second main result. For clause sets<br>including the definition of an equivalence relation with the help of an<br>additional, novel approximation, called reflexive relation splitting, the<br>approximation refinement calculus can automatically show satisfiability through<br>the MSLH clause set formalism.<br> %K Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A Tourret, Sophie %A Cropper, Andrew %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T SLD-Resolution Reduction of Second-Order Horn Fragments : %G eng %U http://hdl.handle.net/21.11116/0000-0002-D2B3-6 %R 10.1007/978-3-030-19570-0_17 %D 2019 %B 16th European Conference on Logics in Artificial Intelligence %Z date of event: 2019-05-08 - 2019-05-10 %C Rende, Italy %B Logics in Artificial Intelligence %E Calimeri, Francesco; Leone, Nicola; Manna, Marco %P 259 - 276 %I Springer %@ 978-3-030-19569-4 %B Lecture Notes in Artificial Intelligence %N 11468

%0 Thesis %A Voigt, Marco %Y Weidenbach, Christoph %A referee: Gr&#228;del, Erich %A referee: Leitsch, Alexander %A referee: Sturm, Thomas %+ 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 External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Decidable Fragments of First-Order Logic and of First-Order Linear Arithmetic with Uninterpreted Predicates : %G eng %U http://hdl.handle.net/21.11116/0000-0005-4373-E %R 10.22028/D291-28428 %U urn:nbn:de:bsz:291--ds-284280 %F OTHER: hdl:20.500.11880/27767 %I Universit&#228;t des Saarlandes %C Saarbr&#252;cken %D 2019 %P 333 p. %V phd %9 phd %X First-order logic is one of the most prominent formalisms in computer science and mathematics. Since there is no algorithm capable of solving its satisfiability problem, first-order logic is said to be undecidable. The classical decision problem is the quest for a delineation between the decidable and the undecidable parts. The results presented in this thesis shed more light on the boundary and open new perspectives on the landscape of known decidable fragments. In the first part we focus on the new concept of separateness of variables and explore its applicability to the classical decision problem and beyond. Two disjoint sets of first-order variables are separated in a given formula if none of its atoms contains variables from both sets. This notion facilitates the definition of decidable extensions of many well-known decidable first-order fragments. We demonstrate this for several prefix fragments, several guarded fragments, the two-variable fragment, and for the fluted fragment. Although the extensions exhibit the same expressive power as the respective originals, certain logical properties can be expressed much more succinctly. In two cases the succinctness gap cannot be bounded using elementary functions. This fact already hints at computationally hard satisfiability problems. Indeed, we derive non-elementary lower bounds for the separated fragment, an extension of the Bernays-Sch&#246;nfinkel-Ramsey fragment (E*A*-prefix sentences). On the semantic level, separateness of quantified variables may lead to weaker dependences than we encounter in general. We investigate this property in the context of model-checking games. The focus of the second part of the thesis is on linear arithmetic with uninterpreted predicates. Two novel decidable fragments are presented, both based on the Bernays-Sch&#246;nfinkel-Ramsey fragment. On the negative side, we identify several small fragments of the language for which satisfiability is undecidable. %U https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/27767

%0 Report %A Voigt, Marco %+ Automation of Logic, MPI for Informatics, Max Planck Society %T Separateness of Variables - A Novel Perspective on Decidable First-Order Fragments : %G eng %U http://hdl.handle.net/21.11116/0000-0005-8D56-C %U http://arxiv.org/abs/1911.11500 %D 2019 %8 26.11.2019 %X The classical decision problem, as it is understood today, is the quest for a<br>delineation between the decidable and the undecidable parts of first-order<br>logic based on elegant syntactic criteria. In this paper, we treat the concept<br>of separateness of variables and explore its applicability to the classical<br>decision problem. Two disjoint sets of first-order variables are separated in a<br>given formula if variables from the two sets never co-occur in any atom of that<br>formula. This simple notion facilitates extending many well-known decidable<br>first-order fragments significantly and in a way that preserves decidability.<br>We will demonstrate that for several prefix fragments, several guarded<br>fragments, the two-variable fragment, and for the fluted fragment. Altogether,<br>we will investigate nine such extensions more closely. Interestingly, each of<br>them contains the relational monadic first-order fragment without equality.<br>Although the extensions exhibit the same expressive power as the respective<br>originals, certain logical properties can be expressed much more succinctly. In<br>three cases the succinctness gap cannot be bounded using any elementary<br>function.<br> %K Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A Vukmirovi&#263;, Petar %A Blanchette, Jasmin Christian %A Cruanes, Simon %A Schulz, Stephan %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Extending a Brainiac Prover to Lambda-Free Higher-Order Logic : %G eng %U http://hdl.handle.net/21.11116/0000-0004-0326-E %R 10.1007/978-3-030-17462-0_11 %D 2019 %B 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems %Z date of event: 2019-04-06 - 2019-04-11 %C Prague, Czech Republic %B Tools and Algorithms for the Construction and Analysis of Systems %P 192 - 210 %I Springer %@ 978-3-030-17461-3 %B Lecture Notes in Computer Science %N 11427

%0 Journal Article %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society %T The Challenge of Unifying Semantic and Syntactic Inference Restrictions : %G eng %U http://hdl.handle.net/21.11116/0000-0005-8750-8 %U https://arxiv.org/abs/1912.12966 %R 10.4204/EPTCS.311.1 %7 2019 %D 2019 %X While syntactic inference restrictions don't play an important role for SAT,<br>they are an essential reasoning technique for more expressive logics, such as<br>first-order logic, or fragments thereof. In particular, they can result in<br>short proofs or model representations. On the other hand, semantically guided<br>inference systems enjoy important properties, such as the generation of solely<br>non-redundant clauses. I discuss to what extend the two paradigms may be<br>unifiable.<br> %K Computer Science, Logic in Computer Science, cs.LO %J Electronic Proceedings in Theoretical Computer Science %O EPTCS %V 311 %& 5 %P 5 - 10 %B Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements %O ARCADE 2019 Natal, Brazil, August 26, 2019

%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

%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

%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

%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

%0 Journal Article %A Boulier, Fran&#231;ois %A Fages, Fran&#231;ois %A Radulescu, Ovidiu %A Samal, Satya Swarup %A Schuppert, Andreas %A Seiler, Werner %A Sturm, Thomas %A Walcher, Sebastian %A Weber, Andreas %+ External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T The SYMBIONT Project: Symbolic Methods for Biological Networks : %G eng %U http://hdl.handle.net/21.11116/0000-0002-E8C2-D %R 10.7490/f1000research.1115995.1 %7 2018 %D 2018 %J Faculty of 1000 Research %O F1000Research %V 7 %Z sequence number: 1341 %I BioMed Central %C London %@ false %U https://doi.org/10.7490/f1000research.1115995.1

%0 Journal Article %A Boulier, Fran&#231;ois %A Fages, Fran&#231;ois %A Radulescu, Ovidiu %A Samal, Satya Swarup %A Schuppert, Andreas %A Seiler, Werner %A Sturm, Thomas %A Walcher, Sebastian %A Weber, Andreas %+ External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T The SYMBIONT Project: Symbolic Methods for Biological Networks : %G eng %U http://hdl.handle.net/21.11116/0000-0002-F07D-3 %R 10.1145/3313880.3313885 %7 2018 %D 2018 %J ACM Communications in Computer Algebra %V 52 %N 3 %& 67 %P 67 - 70 %I ACM %C New York, NY %@ false

%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

%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

%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&#233;r&#244;me %P 5588 - 5592 %I IJCAI %@ 978-0-9992411-2-7

%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

%0 Conference Proceedings %A Fontaine, Pascal %A Ogawa, Mizuhito %A Sturm, Thomas %A To, Van Khanh %A Vu, Xuan Tung %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT : %G eng %U http://hdl.handle.net/21.11116/0000-0002-E8AB-8 %D 2018 %B 3rd Workshop on Satisfiability Checking and Symbolic Computation %Z date of event: 2018-07-11 - 2018-07-11 %C Oxford, UK %B Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation co-located with Federated Logic Conference %E Bigatti, Anna M.; Brain, Martin %P 110 - 117 %Z sequence number: 3 %I CEUR-WS %B CEUR Workshop Proceedings %N 2189 %U http://ceur-ws.org/Vol-2189/paper3.pdf

%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<br>reals. All polynomial coefficients are parameters ranging over the reals, where<br>for each coefficient we prescribe its sign. We are interested in the existence<br>of positive real solutions of our system for all choices of coefficients<br>subject to our sign conditions. We give a decision procedure for the existence<br>of such solutions. In the positive case our procedure yields a parametric<br>positive solution as a rational function in the coefficients. Our framework<br>allows to reformulate heuristic subtropical approaches for non-parametric<br>systems of polynomial inequalities that have been recently used in qualitative<br>biological network analysis and, independently, in satisfiability modulo theory<br>solving. We apply our results to characterize the incompleteness of those<br>methods.<br> %K Computer Science, Symbolic Computation, cs.SC,Computer Science, Logic in Computer Science, cs.LO

%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

%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 Formalizing 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

%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

%0 Conference Proceedings %A Sturm, Thomas %+ Automation of Logic, MPI for Informatics, Max Planck Society %T Thirty Years of Virtual Substitution: Foundations, Techniques, Applications : %G eng %U http://hdl.handle.net/21.11116/0000-0002-E8D6-7 %R 10.1145/3208976.3209030 %D 2018 %B 43rd International Symposium on Symbolic and Algebraic Computation %Z date of event: 2018-07-16 - 2018-07-19 %C New York, NY, USA %B ISSAC'18 %E Arreche, Carlos %P 11 - 16 %I ACM %@ 978-1-4503-5550-6

%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 %F OTHER: hdl:20.500.11880/27069 %I Universit&#228;t des Saarlandes %C Saarbr&#252;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-<br>order logic, I have developed an approximation theorem proving approach based on<br>counterexample-guided abstraction refinement. A given clause set is transformed<br>into a simplified form where satisfiability is decidable. This approximation extends<br>the signature and preserves unsatisfiability: if the simplified clause set is satisfi-<br>able, so is the original clause set. A resolution refutation generated by a decision<br>procedure on the simplified clause set can then either be lifted to a refutation in<br>the original clause set, or it guides a refinement excluding the previously found<br>unliftable refutation. This way the approach is refutationally complete.<br>The monadic shallow linear Horn fragment, which is the initial target of the<br>approximation, is well-known to be decidable. It was a long standing open prob-<br>lem how to extend the fragment to the non-Horn case, preserving decidability, that<br>would, e.g., enable to express non-determinism in protocols. I have now proven de-<br>cidability of the non-Horn monadic shallow linear fragment via ordered resolution.<br>I further extend the clause language with a new type of constraints, called<br>straight dismatching constraints. The extended clause language is motivated by an<br>improved refinement of the approximation-refinement framework. All needed oper-<br>ations on straight dismatching constraints take linear or linear logarithmic time in<br>the size of the constraint. Ordered resolution with straight dismatching constraints<br>is sound and complete and the monadic shallow linear fragment with straight dis-<br>matching constraints is decidable.<br>I have implemented my approach based on the SPASS theorem prover. On cer-<br>tain satisfiable problems, the implementation shows the ability to beat established<br>provers such as SPASS, iProver, and Vampire. %U https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/27069

%0 Journal Article %A Althaus, Ernst %A Beber, Bj&#246;rn %A Damm, Werner %A Disch, Stefan %A Hagemann, Willem %A Rakow, Astrid %A Scholl, Christoph %A Waldmann, Uwe %A Wirtz, Boris %+ Algorithms and Complexity, MPI for Informatics, Max Planck Society Algorithms and Complexity, MPI for Informatics, Max Planck Society External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Verification of Linear Hybrid Systems with Large Discrete State Spaces Using Counterexample-guided Abstraction Refinement : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002E-1C23-5 %R 10.1016/j.scico.2017.04.010 %7 2017-05-10 %D 2017 %J Science of Computer Programming %V 148 %& 123 %P 123 - 160 %I Elsevier %C Amsterdam %@ false

%0 Journal Article %A Barbosa, Haniel %A Blanchette, Jasmin Christian %A Cruanes, Simon %A El Ouraoui, Daniel %A Fontaine, Pascal %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations %T Language and Proofs for Higher-Order SMT (Work in Progress) : %G eng %U http://hdl.handle.net/21.11116/0000-0000-64DD-7 %R 10.4204/EPTCS.262.3 %U http://arxiv.org/abs/1712.01486 %7 2017 %D 2017 %X Satisfiability modulo theories (SMT) solvers have throughout the years been<br>able to cope with increasingly expressive formulas, from ground logics to full<br>first-order logic modulo theories. Nevertheless, higher-order logic within SMT<br>is still little explored. One main goal of the Matryoshka project, which<br>started in March 2017, is to extend the reasoning capabilities of SMT solvers<br>and other automatic provers beyond first-order logic. In this preliminary<br>report, we report on an extension of the SMT-LIB language, the standard input<br>format of SMT solvers, to handle higher-order constructs. We also discuss how<br>to augment the proof format of the SMT solver veriT to accommodate these new<br>constructs and the solving techniques they require.<br> %K Computer Science, Logic in Computer Science, cs.LO %J Electronic Proceedings in Theoretical Computer Science %O EPTCS %V 262 %& 15 %P 15 - 22

%0 Conference Proceedings %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/11858/00-001M-0000-002E-0713-5 %R 10.1007/978-3-319-63046-5_25 %D 2017 %B 26th International Conference on Automated Deduction %Z date of event: 2017-08-06 - 2017-08-11 %C Gothenburg, Sweden %B Automated Deduction -- CADE 26 %E de Moura, Leonardo %P 398 - 412 %I Springer %@ 978-3-319-63045-8 %B Lecture Notes in Artificial Intelligence %N 10395

%0 Journal Article %A Barkatou, Moulay A. %A Jaroschek, Maximilian %A Maddah, Suzy S. %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-6564-9 %R 10.1016/j.jsc.2016.11.018 %7 2016-11-18 %D 2017 %J Journal of Symbolic Computation %V 81 %& 41 %P 41 - 68 %I Elsevier %C Amsterdam %@ false

%0 Conference Proceedings %A Becker, Heiko %A Blanchette, Jasmin Christian %A Waldmann, Uwe %A Wand, Daniel %+ External Organizations 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 A Transfinite Knuth&#8211;Bendix Order for Lambda-Free Higher-Order Terms : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002E-0711-9 %R 10.1007/978-3-319-63046-5_27 %D 2017 %B 26th International Conference on Automated Deduction %Z date of event: 2017-08-06 - 2017-08-11 %C Gothenburg, Sweden %B Automated Deduction -- CADE 26 %E de Moura, Leonardo %P 432 - 453 %I Springer %@ 978-3-319-63045-8 %B Lecture Notes in Artificial Intelligence %N 10395

%0 Conference Proceedings %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Klakow, Dietrich %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T A Formal Proof of the Expressiveness of Deep Learning : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002E-06F8-9 %R 10.1007/978-3-319-66107-0_4 %D 2017 %B 8th Conference on Interactive Theorem Proving %Z date of event: 2017-09-26 - 2017-09-29 %C Brasilia, Brazil %B Interactive Theorem Proving %E Avala-Rinc&#243;n, Mauricio; Mu&#241;oz, C&#233;sar A. %P 46 - 64 %I Springer %@ 978-3-319-66106-3 %B Lecture Notes in Computer Science %N 10499

%0 Conference Proceedings %A Biendarra, Julian %A Blanchette, Jasmin Christian %A Bouzy, Aymeric %A Desharnais, Martin %A Fleury, Mathias %A H&#246;lzl, Johannes %A Kun&#269;ar, Ond&#345;ej %A Lochbihler, Andreas %A Meier, Fabian %A Panny, Lorenz %A Popescu, Andrei %A Sternagel, Christian %A Thiemann, Ren&#233; %A Traytel, Dmitriy %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations %T Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002E-070E-4 %R 10.1007/978-3-319-66167-4_1 %D 2017 %B 11th International Symposium on Frontiers of Combining Systems %Z date of event: 2017-09-27 - 2017-09-29 %C Bras&#237;lia, Brazil %B Frontiers of Combining Systems %E Dixon, Clare; Finger, Marcelo %P 3 - 21 %I Springer %@ 978-3-319-66166-7 %B Lecture Notes in Artificial Intelligence %N 10483

%0 Journal Article %A Blanchette, Jasmin Christian %A Popescu, Andrei %A Traytel, Dmitriy %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Soundness and Completeness Proofs by Coinductive Methods : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-3B94-0 %R 10.1007/s10817-016-9391-3 %7 2016-10-18 %D 2017 %J Journal of Automated Reasoning %V 58 %N 1 %& 149 %P 149 - 179 %I Springer %C London %@ false

%0 Journal Article %A Blanchette, Jasmin Christian %A Popescu, Andrei %A Traytel, Dmitriy %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Abstract Soundness : %G eng %U http://hdl.handle.net/21.11116/0000-0000-64A8-2 %7 2017 %D 2017 %J Archive of Formal Proofs %& 1 %P 1 - 15 %@ false %U https://www.isa-afp.org/browser_info/current/AFP/Abstract_Soundness/document.pdf

%0 Conference Proceedings %A Blanchette, Jasmin Christian %A Waldmann, Uwe %A Wand, Daniel %+ 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 A Lambda-Free Higher-Order Recursive Path Order : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-91BA-2 %R 10.1007/978-3-662-54458-7_27 %D 2017 %B 20th International Conference on Foundations of Software Science and Computation Structures %Z date of event: 2017-04-24 - 2017-04-27 %C Uppsala, Sweden %B Foundations of Software Science and Computation Structures %E Esparza, Javier; Murawski, Andrzej S. %P 461 - 479 %I Springer %@ 978-3-662-54457-0 %B Lecture Notes in Computer Science %N 10203

%0 Conference Proceedings %A Blanchette, Jasmin Christian %A Fleury, Mathias %A Weidenbach, Christoph %+ 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 A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002E-0702-B %R 10.24963/ijcai.2017/667 %D 2017 %B Twenty-Sixth International Joint Conference on Artificial Intelligence %Z date of event: 2017-08-19 - 2017-08-25 %C Melbourne, Australia %B Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence %E Sierra, Carles %P 4786 - 4790 %I International Joint Conferences on Artificial Intelligence %@ 978-3-319-40228-4

%0 Conference Proceedings %A Blanchette, Jasmin Christian %A Fontaine, Pascal %A Schulz, Stephan %A Waldmann, Uwe %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Towards Strong Higher-Order Automation for Fast Interactive Verification : %G eng %U http://hdl.handle.net/21.11116/0000-0000-64CF-7 %R 10.29007/3ngx %D 2017 %B 1st International Workshop on Automated Reasoning %Z date of event: 2017-08-06 - 2017-08-06 %C Gothenburg, Sweden %B ARCADE 2017 %E Reger, Giles; Traytel, Dmitriy %P 16 - 23 %B EPiC Series in Computing %N 51

%0 Conference Proceedings %A Blanchette, Jasmin Christian %A Fleury, Mathias %A Traytel, Dmitriy %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002E-06EE-1 %R 10.4230/LIPIcs.FSCD.2017.11 %U urn:nbn:de:0030-drops-77155 %D 2017 %B 2nd International Conference on Formal Structures for Computation and Deduction %Z date of event: 2017-09-03 - 2017-09-09 %C Oxford, UK %B 2nd International Conference on Formal Structures for Computation and Deduction %E Miller, Dale %P 1 - 18 %Z sequence number: 1 %I Schloss Dagstuhl %@ 978-3-95977-047-7 %B Leibniz International Proceedings in Informatics %N 84 %@ false %U http://drops.dagstuhl.de/opus/volltexte/2017/7715/http://drops.dagstuhl.de/doku/urheberrecht1.html

%0 Conference Proceedings %A Bradford, Russell %A Davenport, James H. %A England, Matthew %A Errami, Hassan %A Gerdt, Vladimir %A Grigoriev, Dima %A Hoyt, Charles %A Ko&#353;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 A Case Study on the Parametric Occurrence of Multiple Steady States : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002E-07B0-1 %R 10.1145/3087604.3087622 %D 2017 %B International Symposium on Symbolic and Algebraic Computation %Z date of event: 2017-07-25 - 2017-07-28 %C Kaiserslautern, Germany %B ISSAC&#8217;17 %P 45 - 52 %I ACM %@ 978-1-4503-5064-8

%0 Report %A Bradford, Russell %A Davenport, James H. %A England, Matthew %A Errami, Hassan %A Gerdt, Vladimir %A Grigoriev, Dima %A Hoyt, Charles %A Ko&#353;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 A Case Study on the Parametric Occurrence of Multiple Steady States : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-91D0-E %U http://arxiv.org/abs/1704.08997 %D 2017 %X We consider the problem of determining multiple steady states for positive real values in models of biological networks. Investigating the potential for these in models of the mitogen-activated protein kinases (MAPK) network has consumed considerable effort using special insights into the structure of corresponding models. Here we apply combinations of symbolic computation methods for mixed equality/inequality systems, specifically virtual substitution, lazy real triangularization and cylindrical algebraic decomposition. We determine multistationarity of an 11-dimensional MAPK network when numeric values are known for all but potentially one parameter. More precisely, our considered model has 11 equations in 11 variables and 19 parameters, 3 of which are of interest for symbolic treatment, and furthermore positivity conditions on all variables and parameters. %K Computer Science, Symbolic Computation, cs.SC

%0 Journal Article %A Bromberger, Martin %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T New Techniques for Linear Arithmetic: Cubes and Equalities : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002E-260E-C %R 10.1007/s10703-017-0278-7 %7 2017 %D 2017 %J Formal Methods in System Design %V 51 %N 3 %& 433 %P 433 - 461 %I Springer %C Berlin %@ false

%0 Journal Article %A Demri, St&#233;phane %A Kapur, Deepak %A Weidenbach, Christoph %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Preface -Special Issue of Selected Extended Papers of IJCAR 2014 : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-4CD1-C %R 10.1007/s10817-016-9394-0 %7 2016 %D 2017 %J Journal of Automated Reasoning %V 58 %N 1 %& 1 %P 1 - 2 %I D. Reidel Pub. Co. %C Dordrecht, Holland %@ false

%0 Journal Article %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-0000-C8DF-4 %R 10.1613/jair.5481 %7 2017 %D 2017 %J Journal of Artificial Intelligence Research %V 60 %& 827 %P 827 - 880 %I AI Access Foundation %C S.l. %@ false

%0 Report %A England, Matthew %A Errami, Hassan %A Grigoriev, Dima %A Radulescu, Ovidiu %A Sturm, Thomas %A Weber, Andreas %+ External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-91C9-F %U http://arxiv.org/abs/1706.08794 %D 2017 %X We investigate models of the mitogenactivated protein kinases (MAPK) network, with the aim of determining where in parameter space there exist multiple positive steady states. We build on recent progress which combines various symbolic computation methods for mixed systems of equalities and inequalities. We demonstrate that those techniques benefit tremendously from a newly implemented graph theoretical symbolic preprocessing method. We compare computation times and quality of results of numerical continuation methods with our symbolic approach before and after the application of our preprocessing. %K Computer Science, Symbolic Computation, cs.SC

%0 Conference Proceedings %A England, Matthew %A Errami, Hassan %A Grigoriev, Dima %A Radulescu, Ovidiu %A Sturm, Thomas %A Weber, Andreas %+ External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002E-07A0-5 %R 10.1007/978-3-319-66320-3_8 %D 2017 %B 19th International Workshop on Computer Algebra in Scientific Computing %Z date of event: 2017-09-18 - 2017-09-22 %C Beijing, China %B Computer Algebra in Scientific Computing %E Gerdt, Vladimir P.; Koepf, Wolfram; Seiler, Werner M.; Vorozhtsov, Evgenii V. %P 93 - 108 %I Springer %@ 978-3-319-66319-7 %B Lecture Notes in Computer Science %N 10490

%0 Report %A Fontaine, Pascal %A Ogawa, Mizuhito %A Sturm, Thomas %A Vu, Xuan Tung %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Subtropical Satisfiability : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-91C2-E %U http://arxiv.org/abs/1706.09236 %D 2017 %X Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning for corresponding constraints in SMT theory solvers is highly relevant. We propose a new incomplete but efficient and terminating method to identify satisfiable instances. The method is derived from the subtropical method recently introduced in the context of symbolic computation for computing real zeros of single very large multivariate polynomials. Our method takes as input conjunctions of strict polynomial inequalities, which represent more than 40% of the QF_NRA section of the SMT-LIB library of benchmarks. The method takes an abstraction of polynomials as exponent vectors over the natural numbers tagged with the signs of the corresponding coefficients. It then uses, in turn, SMT to solve linear problems over the reals to heuristically find suitable points that translate back to satisfying points for the original problem. Systematic experiments on the SMT-LIB demonstrate that our method is not a sufficiently strong decision procedure by itself but a valuable heuristic to use within a portfolio of techniques. %K Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A Fontaine, Pascal %A Ogawa, Mizuhito %A Sturm, Thomas %A Vu, Xuan Tung %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Subtropical Satisfiability : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002E-07A7-8 %R 10.1007/978-3-319-66167-4_11 %D 2017 %B 11th International Symposium on Frontiers of Combining Systems %Z date of event: 2017-09-27 - 2017-09-29 %C Bras&#237;lia, Brazil %B Frontiers of Combining Systems %E Dixon, Clare; Finger, Marcelo %P 189 - 206 %I Springer %@ 978-3-319-66166-7 %B Lecture Notes in Artificial Intelligence %N 10483

%0 Report %A Horbach, Matthias %A Voigt, Marco %A Weidenbach, Christoph %+ 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 On the Combination of the Bernays-Sch&#246;nfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-8140-2 %U http://arxiv.org/abs/1705.08792 %D 2017 %X In general, first-order predicate logic extended with linear integer arithmetic is undecidable. We show that the Bernays-Sch\"onfinkel-Ramsey fragment ($\exists^* \forall^*$-sentences) extended with a restricted form of linear integer arithmetic is decidable via finite ground instantiation. The identified ground instances can be employed to restrict the search space of existing automated reasoning procedures considerably, e.g., when reasoning about quantified properties of array data structures formalized in Bradley, Manna, and Sipma's array property fragment. Typically, decision procedures for the array property fragment are based on an exhaustive instantiation of universally quantified array indices with all the ground index terms that occur in the formula at hand. Our results reveal that one can get along with significantly fewer instances. %K Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A Horbach, Matthias %A Voigt, Marco %A Weidenbach, Christoph %+ 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 On the Combination of the Bernays-Sch&#246;nfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-FB27-F %R 10.1007/978-3-319-63046-5_6 %D 2017 %B 26th International Conference on Automated Deduction %Z date of event: 2017-08-06 - 2017-08-11 %C Gothenburg, Sweden %B Automated Deduction -- CADE 26 %E de Moura, Leonardo %P 77 - 94 %I Springer %@ 978-3-319-63045-8 %B Lecture Notes in Artificial Intelligence %N 10395

%0 Report %A Horbach, Matthias %A Voigt, Marco %A Weidenbach, Christoph %+ 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 The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-A5E7-D %U http://arxiv.org/abs/1703.01212 %D 2017 %X The first-order theory of addition over the natural numbers, known as Presburger arithmetic, is decidable in double exponential time. Adding an uninterpreted unary predicate to the language leads to an undecidable theory. We sharpen the known boundary between decidable and undecidable in that we show that the purely universal fragment of the extended theory is already undecidable. Our proof is based on a reduction of the halting problem for two-counter machines to unsatisfiability of sentences in the extended language of Presburger arithmetic that does not use existential quantification. On the other hand, we argue that a single $\forall\exists$ quantifier alternation turns the set of satisfiable sentences of the extended language into a $\Sigma^1_1$-complete set. Some of the mentioned results can be transfered to the realm of linear arithmetic over the ordered real numbers. This concerns the undecidability of the purely universal fragment and the $\Sigma^1_1$-hardness for sentences with at least one quantifier alternation. Finally, we discuss the relevance of our results to verification. In particular, we derive undecidability results for quantified fragments of separation logic, the theory of arrays, and combinations of the theory of equality over uninterpreted functions with restricted forms of integer arithmetic. In certain cases our results even imply the absence of sound and complete deductive calculi. %K Computer Science, Logic in Computer Science, cs.LO

%0 Journal Article %A Lamotte-Schubert, Manuel %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T BDI: A New Decidable Clause Class : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0024-C365-F %R 10.1093/logcom/exu074 %7 2017 %D 2017 %J Journal of Logic and Computation %V 27 %N 2 %& 441 %P 441 - 468 %I Oxford University Press %C Oxford %@ false

%0 Journal Article %A Reynolds, Andrew %A Blanchette, Jasmin Christian %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T A Decision Procedure for (Co)datatypes in SMT Solvers : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-80D4-C %R 10.1007/s10817-016-9372-6 %7 2017 %D 2017 %J Journal of Automated Reasoning %V 58 %N 3 %& 341 %P 341 - 362 %I Springer %C New York, NY %@ false

%0 Journal Article %A Sturm, Thomas %+ Automation of Logic, MPI for Informatics, Max Planck Society %T A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-A3B5-B %R 10.1007/s11786-017-0319-z %7 2017 %D 2017 %J Mathematics in Computer Science %V 11 %N 3-4 %& 483 %P 483 - 502 %I Springer %C New York, NY

%0 Thesis %A Tang, Ching Hoo %Y Weidenbach, Christoph %A referee: Herzig, Andreas %+ 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 Logics for Rule-based Configuration Systems : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002E-0871-7 %U urn:nbn:de:bsz:291-scidok-69639 %R 10.22028/D291-26856 %F OTHER: hdl:20.500.11880/26869 %I Universit&#228;t des Saarlandes %C Saarbr&#252;cken %D 2017 %P X, 123 p. %V phd %9 phd %X Rule-based configuration systems are being successfully used in industry, such as DOPLER at Siemens. Those systems make complex domain knowledge available to users and let them derive valid, customized products out of large sets of components. However, maintenance of such systems remains a challenge. Formal models are a prerequisite for the use of automated methods of analysis. This thesis deals with the formalization of rule-based configuration. We develop two logics whose transition semantics are suited for expressing the way systems like DOPLER operate. This is due to the existence of two types of transitions, namely user and rule transitions, and a fixpoint mechanism that determines their dynamic relationship. The first logic, PIDL, models propositional systems, while the second logic, PIDL+, additionally considers arithmetic constraints. They allow the formulation and automated verification of relevant properties of rule- based configuration systems. %U http://scidok.sulb.uni-saarland.de/volltexte/2017/6963/http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=de

%0 Report %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 Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-A213-1 %U http://arxiv.org/abs/1703.02837 %D 2017 %X The monadic shallow linear Horn fragment is well-known to be decidable and has many application, e.g., in security protocol analysis, tree automata, or abstraction refinement. It was a long standing open problem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. We prove decidability of the non-Horn monadic shallow linear fragment via ordered resolution further extended with dismatching constraints and discuss some applications of the new decidable fragment. %K Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %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 Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-FB2A-9 %R 10.1007/978-3-319-63046-5_13 %D 2017 %B 26th International Conference on Automated Deduction %Z date of event: 2017-08-06 - 2017-08-11 %C Gothenburg, Sweden %B Automated Deduction -- CADE 26 %E de Moura, Leonardo %P 202 - 219 %I Springer %@ 978-3-319-63045-8 %B Lecture Notes in Artificial Intelligence %N 10395

%0 Conference Proceedings %A Voigt, Marco %+ Automation of Logic, MPI for Informatics, Max Planck Society %T The Bernays-Sch&#246;nfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable : %G eng %U http://hdl.handle.net/21.11116/0000-0001-E6DE-2 %R 10.1007/978-3-319-66167-4_14 %D 2017 %B 11th International Symposium on Frontiers of Combining Systems %Z date of event: 2017-09-27 - 2017-09-29 %C Bras&#237;lia, Brazil %B Frontiers of Combining Systems %E Dixon, Clare; Finger, Marcelo %P 244 - 261 %I Springer %@ 978-3-319-66166-7 %B Lecture Notes in Artificial Intelligence %N 10483

%0 Conference Proceedings %A Voigt, Marco %+ Automation of Logic, MPI for Informatics, Max Planck Society %T A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-EFA6-4 %R 10.1109/LICS.2017.8005094 %D 2017 %B 32nd Annual ACM-IEEE Symposium on Logic in Computer Science %Z date of event: 2017-06-20 - 2017-06-23 %C Reykjavik, Iceland %B 32nd Annual ACM-IEEE Symposium on Logic in Computer Science %P 1 - 12 %I ACM %@ 978-1-5090-3019-4

%0 Report %A Voigt, Marco %+ Automation of Logic, MPI for Informatics, Max Planck Society %T The Bernays-Sch&#246;nfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable : %G eng %U http://hdl.handle.net/21.11116/0000-0002-EFBD-D %U http://arxiv.org/abs/1706.08504 %D 2017 %X First-order linear real arithmetic enriched with uninterpreted predicate<br>symbols yields an interesting modeling language. However, satisfiability of<br>such formulas is undecidable, even if we restrict the uninterpreted predicate<br>symbols to arity one. In order to find decidable fragments of this language, it<br>is necessary to restrict the expressiveness of the arithmetic part. One<br>possible path is to confine arithmetic expressions to difference constraints of<br>the form $x - y \mathrel{\#} c$, where $\#$ ranges over the standard relations<br>$<, \leq, =, \neq, \geq, >$ and $x,y$ are universally quantified. However, it<br>is known that combining difference constraints with uninterpreted predicate<br>symbols yields an undecidable satisfiability problem again. In this paper, it<br>is shown that satisfiability becomes decidable if we in addition bound the<br>ranges of universally quantified variables. As bounded intervals over the reals<br>still comprise infinitely many values, a trivial instantiation procedure is not<br>sufficient to solve the problem.<br> %K Computer Science, Logic in Computer Science, cs.LO

%0 Report %A Voigt, Marco %+ Automation of Logic, MPI for Informatics, Max Planck Society %T On Generalizing Decidable Standard Prefix Classes of First-Order Logic : %G eng %U http://hdl.handle.net/21.11116/0000-0002-EFAE-E %U http://arxiv.org/abs/1706.03949 %D 2017 %X Recently, the separated fragment (SF) of first-order logic has been<br>introduced. Its defining principle is that universally and existentially<br>quantified variables may not occur together in atoms. SF properly generalizes<br>both the Bernays-Sch\"onfinkel-Ramsey (BSR) fragment and the relational monadic<br>fragment. In this paper the restrictions on variable occurrences in SF<br>sentences are relaxed such that universally and existentially quantified<br>variables may occur together in the same atom under certain conditions. Still,<br>satisfiability can be decided. This result is established in two ways: firstly,<br>by an effective equivalence-preserving translation into the BSR fragment, and,<br>secondly, by a model-theoretic argument.<br> Slight modifications to the described concepts facilitate the definition of<br>other decidable classes of first-order sentences. The paper presents a second<br>fragment which is novel, has a decidable satisfiability problem, and properly<br>contains the Ackermann fragment and---once more---the relational monadic<br>fragment. The definition is again characterized by restrictions on the<br>occurrences of variables in atoms. More precisely, after certain<br>transformations, Skolemization yields only unary functions and constants, and<br>every atom contains at most one universally quantified variable. An effective<br>satisfiability-preserving translation into the monadic fragment is devised and<br>employed to prove decidability of the associated satisfiability problem.<br> %K Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A Voigt, Marco %+ Automation of Logic, MPI for Informatics, Max Planck Society %T Towards Elimination of Second-Order Quantifiers in the Separated Fragment : %G eng %U http://hdl.handle.net/21.11116/0000-0002-EFA3-9 %D 2017 %B Workshop on Second-Order Quantifier Elimination and Related Topics %Z date of event: 2018-12-06 - 2018-12-08 %C Dresden, Germany %B Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics %E Koopmann, Patrick; Rudolph, Sebastian; Schmidt, Renate A.; Wernhard, Christoph %P 67 - 81 %Z sequence number: 16 %I CEUR-WS %B CEUR Workshop Proceedings %N 2013 %U http://ceur-ws.org/Vol-2013/paper16.pdf

%0 Report %A Voigt, Marco %+ Automation of Logic, MPI for Informatics, Max Planck Society %T A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment : %U http://hdl.handle.net/11858/00-001M-0000-002C-EFA0-0 %U http://arxiv.org/abs/1704.02145 %D 2017 %X Recently, the separated fragment (SF) has been introduced and proved to be decidable. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. The known upper bound on the time required to decide SF's satisfiability problem is formulated in terms of quantifier alternations: Given an SF sentence $\exists \vec{z} \forall \vec{x}_1 \exists \vec{y}_1 \ldots \forall \vec{x}_n \exists \vec{y}_n . \psi$ in which $\psi$ is quantifier free, satisfiability can be decided in nondeterministic $n$-fold exponential time. In the present paper, we conduct a more fine-grained analysis of the complexity of SF-satisfiability. We derive an upper and a lower bound in terms of the degree of interaction of existential variables (short: degree)}---a novel measure of how many separate existential quantifier blocks in a sentence are connected via joint occurrences of variables in atoms. Our main result is the $k$-NEXPTIME-completeness of the satisfiability problem for the set $SF_{\leq k}$ of all SF sentences that have degree $k$ or smaller. Consequently, we show that SF-satisfiability is non-elementary in general, since SF is defined without restrictions on the degree. Beyond trivial lower bounds, nothing has been known about the hardness of SF-satisfiability so far. %K Computer Science, Logic in Computer Science, cs.LO

%0 Thesis %A Wand, Daniel %Y Weidenbach, Christoph %A referee: Blanchette, Jasmin Christian %A referee: Sutcliffe, Geoff %+ 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 Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Superposition: Types and Induction : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-E99C-5 %U urn:nbn:de:bsz:291-scidok-69522 %R 10.22028/D291-26789 %F OTHER: hdl:20.500.11880/26802 %I Universit&#228;t des Saarlandes %C Saarbr&#252;cken %D 2017 %P x, 167 p. %V phd %9 phd %X Proof assistants are becoming widespread for formalization of theories both in computer science and mathematics. They provide rich logics with powerful type systems and machine-checked proofs which increase the confidence in the correctness in complicated and detailed proofs.<br>However, they incur a significant overhead compared to pen-and-paper proofs.<br>This thesis describes work on bridging the gap between high-order proof assistants and first-order automated theorem provers by extending the capabilities of the automated theorem provers to provide features usually found in proof assistants.<br>My first contribution is the development and implementation of a first-order superposition calculus with a polymorphic type system that supports type classes and the accompanying refutational completeness proof for that calculus. The inclusion of the type system into the superposition calculus and solvers completely removes the type encoding overhead when encoding problems from many proof assistants.<br>My second contribution is the development of SupInd, an extension of the typed superposition calculus that supports data types and structural induction over those data types. It includes heuristics that guide the induction and conjecture strengthening techniques, which can be applied independently of the underlying calculus.<br>I have implemented the contributions in a tool called Pirate. The evaluations of both contributions show promising results. %U http://scidok.sulb.uni-saarland.de/volltexte/2017/6952/http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=de

%0 Conference Proceedings %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society %T Do Portfolio Solvers Harm? : %G eng %U http://hdl.handle.net/21.11116/0000-0000-3C43-2 %R 10.29007/vpxm %D 2017 %B 1st International Workshop on Automated Reasoning %Z date of event: 2017-08-06 - 2017-08-06 %C Gothenburg, Sweden %B ARCADE 2017 %E Reger, Giles; Traytel, Dmitriy %P 76 - 81 %B EPiC Series in Computing %N 51

%0 Report %A &#193;brah&#225;m, Erika %A Abbott, John %A Becker, Bernd %A Bigatti, Anna M. %A Brain, Martin %A Buchberger, Bruno %A Cimatti, Alessandro %A Davenport, James H. %A England, Matthew %A Fontaine, Pascal %A Forrest, Stephen %A Griggio, Alberto %A Kroening, Daniel %A Seiler, Werner M. %A Sturm, Thomas %+ External Organizations External Organizations External Organizations External Organizations External Organizations 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 %T SC2: Satisfiability Checking meets Symbolic Computation (Project Paper) : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002B-A967-7 %U http://arxiv.org/abs/1607.08028 %D 2016 %X Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of our newly accepted SC-square project (H2020-FETOPEN-CSA) is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications. In this paper we report on the aims and on the first activities of this project, and formalise some relevant challenges for the unified SC-square community. %K Computer Science, Symbolic Computation, cs.SC,Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A &#193;brah&#225;m, Erika %A Abbott, John %A Becker, Bernd %A Bigatti, Anna M. %A Brain, Martin %A Buchberger, Bruno %A Cimatti, Allesandro %A Davenport, James H. %A England, Matthew %A Fontaine, Pascal %A Forrest, Stephen %A Griggio, Alberto %A Kroening, Daniel %A Seiler, Werner M. %A Sturm, Thomas %+ External Organizations External Organizations External Organizations External Organizations External Organizations 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 %T SC2: Satisfiability Checking Meets Symbolic Computation : Project Paper %G eng %U http://hdl.handle.net/11858/00-001M-0000-002B-0A83-3 %R 10.1007/978-3-319-42547-4_3 %D 2016 %B 9th International Conference on Intelligent Computer Mathematics %Z date of event: 2016-07-25 - 2016-07-29 %C Bialystok, Poland %B Intelligent Computer Mathematics %E Kohlhase, Michael; Johansson, Moa; Miller, Bruce; de Moura, Leonardo; Tompa, Frank %P 28 - 43 %I Springer %@ 978-3-319-42546-7 %B Lecture Notes in Artificial Intelligence %N 9791

%0 Journal Article %A &#193;brah&#225;m, Erika %A Abbott, John %A Becker, Bernd %A Bigatti, Anna M. %A Brain, Martin %A Buchberger, Bruno %A Cimatti, Alessandro %A Davenport, James H. %A England, Matthew %A Fontaine, Pascal %A Forrest, Stephen %A Griggio, Alberto %A Kroening, Daniel %A Seiler, Werner M. %A Sturm, Thomas %+ External Organizations External Organizations External Organizations External Organizations External Organizations 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 %T Satisfiability Checking and Symbolic Computation : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-8ACA-3 %R 10.1145/3055282.3055285 %7 2016 %D 2016 %J ACM Communications in Computer Algebra %V 50 %N 4 %& 145 %P 145 - 147 %I ACM %C New York, NY

%0 Report %A &#193;brah&#225;m, Erika %A Abbott, John %A Becker, Bernd %A Bigatti, Anna M. %A Brain, Martin %A Buchberger, Bruno %A Cimatti, Alessandro %A Davenport, James H. %A England, Matthew %A Fontaine, Pascal %A Forrest, Stephen %A Griggio, Alberto %A Kroening, Daniel %A Seiler, Werner M. %A Sturm, Thomas %+ External Organizations External Organizations External Organizations External Organizations External Organizations 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 %T Satisfiability Checking and Symbolic Computation : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002B-A959-7 %U http://arxiv.org/abs/1607.06945 %D 2016 %X Symbolic Computation and Satisfiability Checking are viewed as individual research areas, but they share common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite these commonalities, the two communities are currently only weakly connected. We introduce a new project SC-square to build a joint community in this area, supported by a newly accepted EU (H2020-FETOPEN-CSA) project of the same name. We aim to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap. This abstract and accompanying poster describes the motivation and aims for the project, and reports on the first activities. %K Computer Science, Symbolic Computation, cs.SC,Computer Science, Logic in Computer Science, cs.LO

%0 Report %A Althaus, Ernst %A Beber, Bj&#246;rn %A Damm, Werner %A Disch, Stefan %A Hagemann, Willem %A Rakow, Astrid %A Scholl, Christoph %A Waldmann, Uwe %A Wirtz, Boris %+ Algorithms and Complexity, MPI for Informatics, Max Planck Society Algorithms and Complexity, MPI for Informatics, Max Planck Society External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society International Max Planck Research School, MPI for Informatics, Max Planck Society External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-4540-0 %Y SFB/TR 14 AVACS %D 2016 %P 93 p. %X This paper provides a suite of optimization techniques for the verification of safety properties of linear hybrid automata with large discrete state spaces, such as naturally arising when incorporating health state monitoring and degradation levels into the controller design. Such models can -- in contrast to purely functional controller models -- not analyzed with hybrid verification engines relying on explicit representations of modes, but require fully symbolic representations for both the continuous and discrete part of the state space. The optimization techniques shown yield consistently a speedup of about 20 against previously published results for a similar benchmark suite, and complement these with new results on counterexample guided abstraction refinement. In combination with the methods guaranteeing preciseness of abstractions, this allows to significantly extend the class of models for which safety can be established, covering in particular models with 23 continuous variables and 2 to the 71 discrete states, 20 continuous variables and 2 to the 199 discrete states, and 9 continuous variables and 2 to the 271 discrete states. %B AVACS Technical Report %N 103 %@ false %U http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_103.pdf

%0 Thesis %A Azmy, Noran %Y Weidenbach, Christoph %A referee: Merz, Stephan %+ 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 A Machine-checked Proof of Correctness of Pastry : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-3BAD-9 %U urn:nbn:de:bsz:291-scidok-67309 %R 10.22028/D291-26683 %F OTHER: hdl:20.500.11880/26739 %I Universit&#228;t des Saarlandes %C Saarbr&#252;cken %D 2016 %P ix, 119 p. %V phd %9 phd %X A distributed hash table (DHT) is a peer-to-peer network that offers the function of a classic hash table, but where different key-value pairs are stored at different nodes on the network. Like a classic hash table, the main function provided by a DHT is key lookup, which retrieves the value stored at a given key.<br>Examples of DHT protocols include Chord, Pastry, Kademlia and Tapestry.<br>Such DHT protocols certain correctness and performance guarantees, but formal verification typically discovers border cases that violate those guarantees. In his PhD thesis, Tianxiang Lu reported correctness problems in published versions of Pastry and developed a model called LuPastry, for which he provided a partial proof of correct delivery of lookup messages assuming no node failure, mechanized in the TLA+ Proof System. In analyzing Lu's proof, I discovered that it contained unproven assumptions, and found counterexamples to several of these assumptions. The contribution of this thesis is threefold. First, I present LuPastry+, a revised TLA+ specification of LuPastry. Aside from needed bug fixes, LuPastry+ contains new definitions that make the specification more modular and significantly improve proof automation. Second, I present a complete TLA+ proof of correct delivery for LuPastry+. Third, I prove that the final step of the node join process of LuPastry/LuPastry+ is not necessary to achieve consistency. In particular, I develop a new specification with a simpler node join process, which I denote by Simplified LuPastry+, and prove correct delivery of lookup messages for this new specification. The proof of correctness of Simplified LuPastry+ is written by reusing the proof for LuPastry+, which represents a success story in proof reuse, especially for proofs of this size.<br>Each of the two proofs amounts to over 32,000 proof steps; to my knowledge, they are currently the largest proofs written in the TLA+ language, and---together with Lu's proof---the only examples of applying full theorem proving for the verification of DHT protocols %U http://scidok.sulb.uni-saarland.de/volltexte/2017/6730/http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=de

%0 Conference Proceedings %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 Rigorous Correctness Proof for Pastry : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002B-01C5-C %R 10.1007/978-3-319-33600-8_5 %D 2016 %B 5th International ABZ Conference %Z date of event: 2016-05-23 - 2016-05-27 %C Linz, Austria %B Abstract State Machines, Alloy, B, TLA, VDM, and Z %E Butler, Michael; Schewe, Klaus-Dieter; Mashkoor, Atif; Biro, Miklos %P 86 - 101 %I Springer %@ 978-3-319-33599-5 %B Lecture Notes in Computer Science %N 9675

%0 Conference Proceedings %E Blanchette, Jasmin Christian %E Kaliszyk , Cezary %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Proceedings First International Workshop on Hammers for Type Theories : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002B-0A70-D %R 10.4204/EPTCS.210 %I EPTCS %D 2016 %B First International Workshop on Hammers for Type Theories %Z date of event: 2016-07-01 - 2016-07-01 %D 2016 %C Coimbra, Portugal %P 35 p. %S Electronic Proceedings in Theoretical Computer Science %V 210 %U http://arxiv.org/abs/1606.05427

%0 Journal Article %A Blanchette, Jasmin Christian %A Kaliszyk, Cezary %A Paulson, Lawrence C. %A Urban, Josef %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations %T Hammering towards QED : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-3A64-6 %R 10.6092/issn.1972-5787/4593 %7 2016 %D 2016 %J Journal of Formalized Reasoning %V 9 %N 1 %& 101 %P 101 - 148 %C Bologna %@ false

%0 Report %A Blanchette, Jasmin Christian %A B&#246;hme, Sascha %A Popescu, Andrei %A Smallbone, Nicholas %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations %T Encoding Monomorphic and Polymorphic Types : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002B-A954-2 %R 10.2168/LMCS-2014-1018 %U http://arxiv.org/abs/1609.08916 %D 2016 %X Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of "cover". The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes. %K Computer Science, Logic in Computer Science, cs.LO

%0 Conference Proceedings %A Blanchette, Jasmin Christian %A Fleury, Mathias %A Weidenbach, Christoph %+ 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 A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002B-01C7-8 %R 10.1007/978-3-319-40229-1_4 %D 2016 %B 8th International Joint Conference on Automated Reasoning %Z date of event: 2016-06-27 - 2016-07-02 %C Coimbra, Portugal %B Automated Reasoning %E Olivetti, Nicola; Tiwari, Ashish %P 25 - 44 %I Springer %@ 978-3-319-40228-4 %B Lecture Notes in Artificial Intelligence %N 9706

%0 Journal Article %A Blanchette, Jasmin Christian %A B&#246;hme, Sascha %A Fleury, Mathias %A Smolka, Steffen Juilf %A Steckermeier, Albert %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Semi-intelligible Isar Proofs from Machine-Generated Proofs : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-C69A-B %R 10.1007/s10817-015-9335-3 %7 2015 %D 2016 %J Journal of Automated Reasoning %V 56 %N 2 %& 155 %P 155 - 200 %I Springer %C Dordrecht %@ false

%0 Journal Article %A Blanchette, Jasmin Christian %A Greenaway, David %A Kaliszyk, Cezary %A K&#252;hlwein, Daniel %A Urban, Josef %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations External Organizations %T A Learning-Based Fact Selector for Isabelle/HOL : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002A-4301-0 %R 10.1007/s10817-016-9362-8 %7 2016 %D 2016 %J Journal of Automated Reasoning %V 57 %N 3 %& 219 %P 219 - 244 %I Springer %C Dordrecht, Holland %@ false

%0 Conference Proceedings %E Blanchette, Jasmin Christian %E Merz, Stephan %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Interactive Theorem Proving : 7th International Conference, ITP 2016 Nancy, France, August 22-25, 2016 ; Proceedings %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-3A6B-7 %@ 978-3-319-43143-7 %R 10.1007/978-3-319-43144-4 %I Springer %D 2016 %B Seventh Conference on Interactive Theorem Proving %Z date of event: 2016-08-22 - 2016-08-27 %D 2016 %C Nancy, France %P XVII, 502 p. %S Lecture Notes in Computer Science %V 9807

%0 Thesis %A Bromberger, Martin %Y Weidenbach, Christoph %A referee: Sturm, Thomas %+ 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 Analysis and Implementation of LIA solvers: CutSAT and BBSAT : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-410C-6 %I Universit&#228;t des Saarlandes %C Saarbr&#252;cken %D 2016 %P 34 p. %V master %9 master

%0 Conference Proceedings %A Bromberger, Martin %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Computing a Complete Basis for Equalities Implied by a System of LRA Constraints : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002B-0AA0-1 %D 2016 %B 14th International Workshop on Satisfiability Modulo Theories %Z date of event: 2016-07-01 - 2016-07-02 %C Coimbra, Portugal %B Satisfiability Modulo Theories %E King, Tim; Piskac, Ruzica %P 15 - 30 %I CEUR-WS.org %B CEUR Workshop Proceedings %N 1617 %@ false %U http://ceur-ws.org/Vol-1617/paper2.pdf

%0 Conference Proceedings %A Bromberger, Martin %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Fast Cube Tests for LIA Constraint Solving : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002B-01C9-4 %R 10.1007/978-3-319-40229-1_9 %D 2016 %B 8th International Joint Conference on Automated Reasoning %Z date of event: 2016-06-27 - 2016-07-02 %C Coimbra, Portugal %B Automated Reasoning %E Olivetti, Nicola; Tiwari, Ashish %P 116 - 132 %I Springer %@ 978-3-319-40228-4 %B Lecture Notes in Artificial Intelligence %N 9706

%0 Conference Proceedings %A Cruanes, Simon %A Blanchette, Jasmin Christian %+ Inria Nancy -- Grand Est Automation of Logic, MPI for Informatics, Max Planck Society %T Extending Nunchaku to Dependent Type Theory : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002B-0A6B-E %R 10.4204/EPTCS.210.3 %U http://arxiv.org/abs/1606.05945 %D 2016 %B First International Workshop on Hammers for Type Theories %Z date of event: 2016-07-01 - 2016-07-01 %C Coimbra, Portugal %X Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone tool, with frontends for various proof assistants. In this short paper, we present some ideas to extend Nunchaku with partial support for dependent types and type classes, to make frontends for Coq and other systems based on dependent type theory more useful. %K Computer Science, Logic in Computer Science, cs.LO %B Proceedings First International Workshop on Hammers for Type Theories %E Blanchette, Jasmin Christian; Kaliszyk , Cezary %P 3 - 12 %B Electronic Proceedings in Theoretical Computer Science %N 210 %@ false

%0 Conference Proceedings %A Fetzer, Christof %A Weidenbach, Christoph %A Wischnewski, Patrick %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Compliance, Functional Safety and Fault Detection by Formal Methods : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-3A6F-0 %R 10.1007/978-3-319-47169-3_48 %D 2016 %B 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation %Z date of event: 2016-10-10 - 2016-10-14 %C Corfu, Greece %B Leveraging Applications of Formal Methods, Verification and Validation %E Margaria, Tiziana; Steffen, Bernhard %P 626 - 632 %I Springer %@ 978-3-319-47168-6 %B Lecture Notes in Computer Science %N 9953

%0 Thesis %A Ko&#353;ta, Marek %Y Sturm, Thomas %A referee: Weber, Andreas %A referee: Weidenbach, Christoph %+ 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 Automation of Logic, MPI for Informatics, Max Planck Society %T New Concepts for Real Quantifier Elimination by Virtual Substitution : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-30A8-9 %R 10.22028/D291-26679 %U urn:nbn:de:bsz:291-scidok-67162 %F OTHER: hdl:20.500.11880/26735 %I Universit&#228;t des Saarlandes %C Saarbr&#252;cken %D 2016 %P xvi, 214 p. %V phd %9 phd %U http://scidok.sulb.uni-saarland.de/volltexte/2016/6716/http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=de

%0 Journal Article %A Ko&#353;ta, Marek %A Sturm, Thomas %A Dolzmann, Andreas %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Better Answers to Real Questions : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0026-A93B-2 %R 10.1016/j.jsc.2015.07.002 %7 2015 %D 2016 %X We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it significantly improves the quality of the results. %K Computer Science, Symbolic Computation, cs.SC,Computer Science, Logic in Computer Science, cs.LO %J Journal of Symbolic Computation %V 74 %& 255 %P 255 - 275 %I Academic Press %C London %@ false

%0 Conference Proceedings %A Reynolds, Andrew %A Blanchette, Jasmin Christian %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T A Decision Procedure for (Co)datatypes in SMT Solvers : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-3A67-F %U http://www.ijcai.org/Proceedings/16/Papers/631.pdf %D 2016 %B 25th International Joint Conference on Artificial Intelligence %Z date of event: 2016-07-09 - 2016-07-15 %C New York, NY, USA %B Twenty-Fifth International Joint Conference on Artificial Intelligence %E Kambhampati, Subbarao %P 4205 - 4209 %Z sequence number: 631 %I AAAI %@ 978-1-57735-771-1

%0 Conference Proceedings %A Reynolds, Andrew %A Blanchette, Jasmin Christian %A Cruanes, Simon %A Tinelli, Cesare %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Model Finding for Recursive Functions in SMT : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002B-0900-2 %R 10.1007/978-3-319-40229-1_10 %D 2016 %B 8th International Joint Conference on Automated Reasoning %Z date of event: 2016-06-27 - 2016-07-02 %C Coimbra, Portugal %B Automated Reasoning %E Olivetti, Nicola; Tiwari, Ashish %P 133 - 151 %I Springer %@ 978-3-319-40228-4 %B Lecture Notes in Artificial Intelligence %N 9706