# The Year Before Last

Althaus, E., Beber, B., Damm, W., Disch, S., Hagemann, W., Rakow, A., … Wirtz, B. (2017). Verification of Linear Hybrid Systems with Large Discrete State Spaces Using Counterexample-guided Abstraction Refinement.

*Science of Computer Programming*,*148*. doi:10.1016/j.scico.2017.04.010Export

BibTeX

@article{Althaus2017,
TITLE = {Verification of Linear Hybrid Systems with Large Discrete State Spaces Using Counterexample-guided Abstraction Refinement},
AUTHOR = {Althaus, Ernst and Beber, Bj{\"o}rn and Damm, Werner and Disch, Stefan and Hagemann, Willem and Rakow, Astrid and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
LANGUAGE = {eng},
ISSN = {0167-6423},
DOI = {10.1016/j.scico.2017.04.010},
PUBLISHER = {Elsevier},
ADDRESS = {Amsterdam},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
JOURNAL = {Science of Computer Programming},
VOLUME = {148},
PAGES = {123--160},
}

Endnote

%0 Journal Article
%A Althaus, Ernst
%A Beber, Bjö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

Barbosa, H., Blanchette, J. C., Cruanes, S., El Ouraoui, D., & Fontaine, P. (2017). Language and Proofs for Higher-Order SMT (Work in Progress).

(arXiv: 1712.01486) *Electronic Proceedings in Theoretical Computer Science*,*262*. doi:10.4204/EPTCS.262.3Abstract

Satisfiability modulo theories (SMT) solvers have throughout the years been
able to cope with increasingly expressive formulas, from ground logics to full
first-order logic modulo theories. Nevertheless, higher-order logic within SMT
is still little explored. One main goal of the Matryoshka project, which
started in March 2017, is to extend the reasoning capabilities of SMT solvers
and other automatic provers beyond first-order logic. In this preliminary
report, we report on an extension of the SMT-LIB language, the standard input
format of SMT solvers, to handle higher-order constructs. We also discuss how
to augment the proof format of the SMT solver veriT to accommodate these new
constructs and the solving techniques they require.

Export

BibTeX

@article{Barbosa1712.01486,
TITLE = {Language and Proofs for Higher-Order {SMT} (Work in Progress)},
AUTHOR = {Barbosa, Haniel and Blanchette, Jasmin Christian and Cruanes, Simon and El Ouraoui, Daniel and Fontaine, Pascal},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1712.01486},
DOI = {10.4204/EPTCS.262.3},
EPRINT = {1712.01486},
EPRINTTYPE = {arXiv},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
ABSTRACT = {Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT is still little explored. One main goal of the Matryoshka project, which started in March 2017, is to extend the reasoning capabilities of SMT solvers and other automatic provers beyond first-order logic. In this preliminary report, we report on an extension of the SMT-LIB language, the standard input format of SMT solvers, to handle higher-order constructs. We also discuss how to augment the proof format of the SMT solver veriT to accommodate these new constructs and the solving techniques they require.},
JOURNAL = {Electronic Proceedings in Theoretical Computer Science},
VOLUME = {262},
PAGES = {15--22},
}

Endnote

%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
able to cope with increasingly expressive formulas, from ground logics to full
first-order logic modulo theories. Nevertheless, higher-order logic within SMT
is still little explored. One main goal of the Matryoshka project, which
started in March 2017, is to extend the reasoning capabilities of SMT solvers
and other automatic provers beyond first-order logic. In this preliminary
report, we report on an extension of the SMT-LIB language, the standard input
format of SMT solvers, to handle higher-order constructs. We also discuss how
to augment the proof format of the SMT solver veriT to accommodate these new
constructs and the solving techniques they require.
%K Computer Science, Logic in Computer Science, cs.LO
%J Electronic Proceedings in Theoretical Computer Science
%O EPTCS
%V 262
%& 15
%P 15 - 22

Barkatou, M. A., Jaroschek, M., & Maddah, S. S. (2017). Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings.

*Journal of Symbolic Computation*,*81*. doi:10.1016/j.jsc.2016.11.018Export

BibTeX

@article{Barkatou2017,
TITLE = {Formal Solutions of Completely Integrable {Pfaffian} Systems With Normal Crossings},
AUTHOR = {Barkatou, Moulay A. and Jaroschek, Maximilian and Maddah, Suzy S.},
LANGUAGE = {eng},
ISSN = {0747-7171},
DOI = {10.1016/j.jsc.2016.11.018},
PUBLISHER = {Elsevier},
ADDRESS = {Amsterdam},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
JOURNAL = {Journal of Symbolic Computation},
VOLUME = {81},
PAGES = {41--68},
}

Endnote

%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

Becker, H., Blanchette, J. C., Waldmann, U., & Wand, D. (2017). A Transfinite Knuth–Bendix Order for Lambda-Free Higher-Order Terms. In

*Automated Deduction -- CADE 26*. Gothenburg, Sweden: Springer. doi:10.1007/978-3-319-63046-5_27Export

BibTeX

@inproceedings{BeckerCADE2017,
TITLE = {A Transfinite {K}nuth--{B}endix Order for Lambda-Free Higher-Order Terms},
AUTHOR = {Becker, Heiko and Blanchette, Jasmin Christian and Waldmann, Uwe and Wand, Daniel},
LANGUAGE = {eng},
ISBN = {978-3-319-63045-8},
DOI = {10.1007/978-3-319-63046-5_27},
PUBLISHER = {Springer},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
BOOKTITLE = {Automated Deduction -- CADE 26},
EDITOR = {de Moura, Leonardo},
PAGES = {432--453},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {10395},
ADDRESS = {Gothenburg, Sweden},
}

Endnote

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

Bentkamp, A., Blanchette, J. C., & Klakow, D. (2017). A Formal Proof of the Expressiveness of Deep Learning. In

*Interactive Theorem Proving (ITP 2017)*. Brasilia, Brazil: Springer. doi:10.1007/978-3-319-66107-0_4Export

BibTeX

@inproceedings{BentkampITP2017,
TITLE = {A Formal Proof of the Expressiveness of Deep Learning},
AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin Christian and Klakow, Dietrich},
LANGUAGE = {eng},
ISBN = {978-3-319-66106-3},
DOI = {10.1007/978-3-319-66107-0_4},
PUBLISHER = {Springer},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
BOOKTITLE = {Interactive Theorem Proving (ITP 2017)},
EDITOR = {Avala-Rinc{\'o}n, Mauricio and Mu{\~n}oz, C{\'e}sar A.},
PAGES = {46--64},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {10499},
ADDRESS = {Brasilia, Brazil},
}

Endnote

%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ón, Mauricio; Muñoz, César A.
%P 46 - 64
%I Springer
%@ 978-3-319-66106-3
%B Lecture Notes in Computer Science
%N 10499

Biendarra, J., Blanchette, J. C., Bouzy, A., Desharnais, M., Fleury, M., Hölzl, J., … Traytel, D. (2017). Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. In

*Frontiers of Combining Systems (FroCoS 2017)*. Brasília, Brazil: Springer. doi:10.1007/978-3-319-66167-4_1Export

BibTeX

@inproceedings{BiendarraFroCoS2017,
TITLE = {Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic},
AUTHOR = {Biendarra, Julian and Blanchette, Jasmin Christian and Bouzy, Aymeric and Desharnais, Martin and Fleury, Mathias and H{\"o}lzl, Johannes and Kun{\v c}ar, Ond{\v r}ej and Lochbihler, Andreas and Meier, Fabian and Panny, Lorenz and Popescu, Andrei and Sternagel, Christian and Thiemann, Ren{\'e} and Traytel, Dmitriy},
LANGUAGE = {eng},
ISBN = {978-3-319-66166-7},
DOI = {10.1007/978-3-319-66167-4_1},
PUBLISHER = {Springer},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
BOOKTITLE = {Frontiers of Combining Systems (FroCoS 2017)},
EDITOR = {Dixon, Clare and Finger, Marcelo},
PAGES = {3--21},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {10483},
ADDRESS = {Bras{\'i}lia, Brazil},
}

Endnote

%0 Conference Proceedings
%A Biendarra, Julian
%A Blanchette, Jasmin Christian
%A Bouzy, Aymeric
%A Desharnais, Martin
%A Fleury, Mathias
%A Hölzl, Johannes
%A Kunčar, Ondřej
%A Lochbihler, Andreas
%A Meier, Fabian
%A Panny, Lorenz
%A Popescu, Andrei
%A Sternagel, Christian
%A Thiemann, René
%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í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

Blanchette, J. C., Fleury, M., & Weidenbach, C. (2017). A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. In

*Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI 2017)*. Melbourne, Australia: International Joint Conferences on Artificial Intelligence. doi:10.24963/ijcai.2017/667Export

BibTeX

@inproceedings{BlanchetteIJCAI2017,
TITLE = {A Verified {SAT} Solver Framework with Learn, Forget, Restart, and Incrementality},
AUTHOR = {Blanchette, Jasmin Christian and Fleury, Mathias and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-319-40228-4},
DOI = {10.24963/ijcai.2017/667},
PUBLISHER = {International Joint Conferences on Artificial Intelligence},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI 2017)},
EDITOR = {Sierra, Carles},
PAGES = {4786--4790},
ADDRESS = {Melbourne, Australia},
}

Endnote

%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

Blanchette, J. C., Fleury, M., & Traytel, D. (2017). Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. In

*2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)*. Oxford, UK: Schloss Dagstuhl. doi:10.4230/LIPIcs.FSCD.2017.11Export

BibTeX

@inproceedings{BlanchetteFSCD2017,
TITLE = {Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in {Isabelle}/{HOL}},
AUTHOR = {Blanchette, Jasmin Christian and Fleury, Mathias and Traytel, Dmitriy},
LANGUAGE = {eng},
ISSN = {1868-8969},
ISBN = {978-3-95977-047-7},
URL = {urn:nbn:de:0030-drops-77155},
DOI = {10.4230/LIPIcs.FSCD.2017.11},
PUBLISHER = {Schloss Dagstuhl},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
EDITOR = {Miller, Dale},
PAGES = {1--18},
EID = {1},
SERIES = {Leibniz International Proceedings in Informatics},
VOLUME = {84},
ADDRESS = {Oxford, UK},
}

Endnote

%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

Blanchette, J. C., Waldmann, U., & Wand, D. (2017). A Lambda-Free Higher-Order Recursive Path Order. In

*Foundations of Software Science and Computation Structures (FoSSaCS 2017)*. Uppsala, Sweden: Springer. doi:10.1007/978-3-662-54458-7_27Export

BibTeX

@inproceedings{BlanchetteFoSSaCS2017,
TITLE = {A Lambda-Free Higher-Order Recursive Path Order},
AUTHOR = {Blanchette, Jasmin Christian and Waldmann, Uwe and Wand, Daniel},
LANGUAGE = {eng},
ISBN = {978-3-662-54457-0},
DOI = {10.1007/978-3-662-54458-7_27},
PUBLISHER = {Springer},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
BOOKTITLE = {Foundations of Software Science and Computation Structures (FoSSaCS 2017)},
EDITOR = {Esparza, Javier and Murawski, Andrzej S.},
PAGES = {461--479},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {10203},
ADDRESS = {Uppsala, Sweden},
}

Endnote

%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

Blanchette, J. C., Popescu, A., & Traytel, D. (2017a). Abstract Soundness.

*Archive of Formal Proofs*.Export

BibTeX

@article{BlanchetteAFP2017,
TITLE = {Abstract Soundness},
AUTHOR = {Blanchette, Jasmin Christian and Popescu, Andrei and Traytel, Dmitriy},
LANGUAGE = {eng},
ISSN = {2150-914X},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
JOURNAL = {Archive of Formal Proofs},
PAGES = {1--15},
}

Endnote

%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

Blanchette, J. C., Popescu, A., & Traytel, D. (2017b). Soundness and Completeness Proofs by Coinductive Methods.

*Journal of Automated Reasoning*,*58*(1). doi:10.1007/s10817-016-9391-3Export

BibTeX

@article{DBLP:journals/jar/BlanchettePT17,
TITLE = {Soundness and Completeness Proofs by Coinductive Methods},
AUTHOR = {Blanchette, Jasmin Christian and Popescu, Andrei and Traytel, Dmitriy},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-016-9391-3},
PUBLISHER = {Springer},
ADDRESS = {London},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {58},
NUMBER = {1},
PAGES = {149--179},
}

Endnote

%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

Blanchette, J. C., Fontaine, P., Schulz, S., & Waldmann, U. (2017). Towards Strong Higher-Order Automation for Fast Interactive Verification. In

*ARCADE 2017*. Gothenburg, Sweden. doi:10.29007/3ngxExport

BibTeX

@inproceedings{Blanchette_ARCADE2017,
TITLE = {Towards Strong Higher-Order Automation for Fast Interactive Verification},
AUTHOR = {Blanchette, Jasmin Christian and Fontaine, Pascal and Schulz, Stephan and Waldmann, Uwe},
LANGUAGE = {eng},
DOI = {10.29007/3ngx},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {ARCADE 2017},
EDITOR = {Reger, Giles and Traytel, Dmitriy},
PAGES = {16--23},
SERIES = {EPiC Series in Computing},
VOLUME = {51},
ADDRESS = {Gothenburg, Sweden},
}

Endnote

%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

Bradford, R., Davenport, J. H., England, M., Errami, H., Gerdt, V., Grigoriev, D., … Weber, A. (2017a). A Case Study on the Parametric Occurrence of Multiple Steady States. In

*ISSAC’17, International Symposium on Symbolic and Algebraic Computation*. Kaiserslautern, Germany: ACM. doi:10.1145/3087604.3087622Export

BibTeX

@inproceedings{BradfordISSAC2017,
TITLE = {A Case Study on the Parametric Occurrence of Multiple Steady States},
AUTHOR = {Bradford, Russell and Davenport, James H. and England, Matthew and Errami, Hassan and Gerdt, Vladimir and Grigoriev, Dima and Hoyt, Charles and Ko{\v s}ta, Marek and Radulescu, Ovidiu and Sturm, Thomas and Weber, Andreas},
LANGUAGE = {eng},
ISBN = {978-1-4503-5064-8},
DOI = {10.1145/3087604.3087622},
PUBLISHER = {ACM},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
BOOKTITLE = {ISSAC{\textquoteright}17, International Symposium on Symbolic and Algebraic Computation},
PAGES = {45--52},
ADDRESS = {Kaiserslautern, Germany},
}

Endnote

%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š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’17
%P 45 - 52
%I ACM
%@ 978-1-4503-5064-8

Bradford, R., Davenport, J. H., England, M., Errami, H., Gerdt, V., Grigoriev, D., … Weber, A. (2017b). A Case Study on the Parametric Occurrence of Multiple Steady States. Retrieved from http://arxiv.org/abs/1704.08997

(arXiv: 1704.08997) Abstract

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.

Export

BibTeX

@online{DBLP:journals/corr/BradfordDEEGGHK17,
TITLE = {A Case Study on the Parametric Occurrence of Multiple Steady States},
AUTHOR = {Bradford, Russell and Davenport, James H. and England, Matthew and Errami, Hassan and Gerdt, Vladimir and Grigoriev, Dima and Hoyt, Charles and Ko{\v s}ta, Marek and Radulescu, Ovidiu and Sturm, Thomas and Weber, Andreas},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1704.08997},
EPRINT = {1704.08997},
EPRINTTYPE = {arXiv},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
ABSTRACT = {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.},
}

Endnote

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

Bromberger, M., & Weidenbach, C. (2017). New Techniques for Linear Arithmetic: Cubes and Equalities.

*Formal Methods in System Design*,*51*(3). doi:10.1007/s10703-017-0278-7Export

BibTeX

@article{Bromberger2017,
TITLE = {New Techniques for Linear Arithmetic: {C}ubes and Equalities},
AUTHOR = {Bromberger, Martin and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0925-9856},
DOI = {10.1007/s10703-017-0278-7},
PUBLISHER = {Springer},
ADDRESS = {Berlin},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
JOURNAL = {Formal Methods in System Design},
VOLUME = {51},
NUMBER = {3},
PAGES = {433--461},
}

Endnote

%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

Demri, S., Kapur, D., & Weidenbach, C. (2017). Preface -Special Issue of Selected Extended Papers of IJCAR 2014.

*Journal of Automated Reasoning*,*58*(1). doi:10.1007/s10817-016-9394-0Export

BibTeX

@article{DBLP:journals/jar/DemriKW17,
TITLE = {Preface -- Special Issue of Selected Extended Papers of {IJCAR} 2014},
AUTHOR = {Demri, St{\'e}phane and Kapur, Deepak and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-016-9394-0},
PUBLISHER = {D. Reidel Pub. Co.},
ADDRESS = {Dordrecht, Holland},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {58},
NUMBER = {1},
PAGES = {1--2},
}

Endnote

%0 Journal Article
%A Demri, Sté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

Echenim, M., Peltier, N., & Tourret, S. (2017). Prime Implicate Generation in Equational Logic.

*Journal of Artificial Intelligence Research*,*60*. doi:10.1613/jair.5481Export

BibTeX

@article{Echenim2017,
TITLE = {Prime Implicate Generation in Equational Logic},
AUTHOR = {Echenim, Mnacho and Peltier, Nicolas and Tourret, Sophie},
LANGUAGE = {eng},
ISSN = {1076-9757},
DOI = {10.1613/jair.5481},
PUBLISHER = {AI Access Foundation},
ADDRESS = {S.l.},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
JOURNAL = {Journal of Artificial Intelligence Research},
VOLUME = {60},
PAGES = {827--880},
}

Endnote

%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

England, M., Errami, H., Grigoriev, D., Radulescu, O., Sturm, T., & Weber, A. (2017a). Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks. In

*Computer Algebra in Scientific Computing*. Beijing, China: Springer. doi:10.1007/978-3-319-66320-3_8Export

BibTeX

@inproceedings{EnglandCASC2017,
TITLE = {Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks},
AUTHOR = {England, Matthew and Errami, Hassan and Grigoriev, Dima and Radulescu, Ovidiu and Sturm, Thomas and Weber, Andreas},
LANGUAGE = {eng},
ISBN = {978-3-319-66319-7},
DOI = {10.1007/978-3-319-66320-3_8},
PUBLISHER = {Springer},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
BOOKTITLE = {Computer Algebra in Scientific Computing},
EDITOR = {Gerdt, Vladimir P. and Koepf, Wolfram and Seiler, Werner M. and Vorozhtsov, Evgenii V.},
PAGES = {93--108},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {10490},
ADDRESS = {Beijing, China},
}

Endnote

%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

England, M., Errami, H., Grigoriev, D., Radulescu, O., Sturm, T., & Weber, A. (2017b). Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks. Retrieved from http://arxiv.org/abs/1706.08794

(arXiv: 1706.08794) Abstract

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.

Export

BibTeX

@online{DBLP:journals/corr/EnglandEGR0017,
TITLE = {Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks},
AUTHOR = {England, Matthew and Errami, Hassan and Grigoriev, Dima and Radulescu, Ovidiu and Sturm, Thomas and Weber, Andreas},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1706.08794},
EPRINT = {1706.08794},
EPRINTTYPE = {arXiv},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
ABSTRACT = {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.},
}

Endnote

%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

Fontaine, P., Ogawa, M., Sturm, T., & Vu, X. T. (2017a). Subtropical Satisfiability. In

*Frontiers of Combining Systems (FroCoS 2017)*. Brasília, Brazil: Springer. doi:10.1007/978-3-319-66167-4_11Export

BibTeX

@inproceedings{FontaineFroCoS2017,
TITLE = {Subtropical Satisfiability},
AUTHOR = {Fontaine, Pascal and Ogawa, Mizuhito and Sturm, Thomas and Vu, Xuan Tung},
LANGUAGE = {eng},
ISBN = {978-3-319-66166-7},
DOI = {10.1007/978-3-319-66167-4_11},
PUBLISHER = {Springer},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
BOOKTITLE = {Frontiers of Combining Systems (FroCoS 2017)},
EDITOR = {Dixon, Clare and Finger, Marcelo},
PAGES = {189--206},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {10483},
ADDRESS = {Bras{\'i}lia, Brazil},
}

Endnote

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

Fontaine, P., Ogawa, M., Sturm, T., & Vu, X. T. (2017b). Subtropical Satisfiability. Retrieved from http://arxiv.org/abs/1706.09236

(arXiv: 1706.09236) Abstract

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.

Export

BibTeX

@online{DBLP:journals/corr/FontaineO0V17,
TITLE = {Subtropical Satisfiability},
AUTHOR = {Fontaine, Pascal and Ogawa, Mizuhito and Sturm, Thomas and Vu, Xuan Tung},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1706.09236},
EPRINT = {1706.09236},
EPRINTTYPE = {arXiv},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
ABSTRACT = {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.},
}

Endnote

%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

Horbach, M., Voigt, M., & Weidenbach, C. (2017a). On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. In

*Automated Deduction -- CADE 26*. Gothenburg, Sweden: Springer. doi:10.1007/978-3-319-63046-5_6Export

BibTeX

@inproceedings{HorbachCADE2017,
TITLE = {On the Combination of the {B}ernays-{S}ch{\"o}nfinkel-{R}amsey Fragment with Simple Linear Integer Arithmetic},
AUTHOR = {Horbach, Matthias and Voigt, Marco and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-319-63045-8},
DOI = {10.1007/978-3-319-63046-5_6},
PUBLISHER = {Springer},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
BOOKTITLE = {Automated Deduction -- CADE 26},
EDITOR = {de Moura, Leonardo},
PAGES = {77--94},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {10395},
ADDRESS = {Gothenburg, Sweden},
}

Endnote

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

Horbach, M., Voigt, M., & Weidenbach, C. (2017b). On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. Retrieved from http://arxiv.org/abs/1705.08792

(arXiv: 1705.08792) Abstract

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.

Export

BibTeX

@online{HorbachArXiv2017,
TITLE = {On the Combination of the Bernays-Sch{\"o}nfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic},
AUTHOR = {Horbach, Matthias and Voigt, Marco and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1705.08792},
EPRINT = {1705.08792},
EPRINTTYPE = {arXiv},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
ABSTRACT = {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.},
}

Endnote

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

Horbach, M., Voigt, M., & Weidenbach, C. (2017c). The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable. Retrieved from http://arxiv.org/abs/1703.01212

(arXiv: 1703.01212) Abstract

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.

Export

BibTeX

@online{VoigtHorbachWeidenbacharXiv2017,
TITLE = {The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable},
AUTHOR = {Horbach, Matthias and Voigt, Marco and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1703.01212},
EPRINT = {1703.01212},
EPRINTTYPE = {arXiv},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
ABSTRACT = {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.},
}

Endnote

%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

Lamotte-Schubert, M., & Weidenbach, C. (2017). BDI: A New Decidable Clause Class.

*Journal of Logic and Computation*,*27*(2). doi:10.1093/logcom/exu074Export

BibTeX

@article{Lamotte-SchubertWeidenbach17,
TITLE = {{BDI}: A New Decidable Clause Class},
AUTHOR = {Lamotte-Schubert, Manuel and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0955-792X},
DOI = {10.1093/logcom/exu074},
PUBLISHER = {Oxford University Press},
ADDRESS = {Oxford},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
JOURNAL = {Journal of Logic and Computation},
VOLUME = {27},
NUMBER = {2},
PAGES = {441--468},
}

Endnote

%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

Reynolds, A., & Blanchette, J. C. (2017). A Decision Procedure for (Co)datatypes in SMT Solvers.

*Journal of Automated Reasoning*,*58*(3). doi:10.1007/s10817-016-9372-6Export

BibTeX

@article{DBLP:journals/jar/ReynoldsB17,
TITLE = {A Decision Procedure for (Co)datatypes in {SMT} Solvers},
AUTHOR = {Reynolds, Andrew and Blanchette, Jasmin Christian},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-016-9372-6},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
JOURNAL = {Journal of Automated Reasoning},
EDITOR = {Kambhampati, Subbarao},
VOLUME = {58},
NUMBER = {3},
PAGES = {341--362},
}

Endnote

%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

Sturm, T. (2017). A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications.

*Mathematics in Computer Science*,*11*(3-4). doi:10.1007/s11786-017-0319-zExport

BibTeX

@article{Sturm2017,
TITLE = {A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications},
AUTHOR = {Sturm, Thomas},
LANGUAGE = {eng},
DOI = {10.1007/s11786-017-0319-z},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
JOURNAL = {Mathematics in Computer Science},
VOLUME = {11},
NUMBER = {3-4},
PAGES = {483--502},
}

Endnote

%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

Tang, C. H. (2017).

*Logics for Rule-based Configuration Systems*. Universität des Saarlandes, Saarbrücken. Retrieved from urn:nbn:de:bsz:291-scidok-69639Abstract

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.

Export

BibTeX

@phdthesis{Tangphd2017,
TITLE = {Logics for Rule-based Configuration Systems},
AUTHOR = {Tang, Ching Hoo},
LANGUAGE = {eng},
URL = {urn:nbn:de:bsz:291-scidok-69639},
SCHOOL = {Universit{\"a}t des Saarlandes},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
ABSTRACT = {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.},
}

Endnote

%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
%I Universität des Saarlandes
%C Saarbrü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

Teucke, A., & Weidenbach, C. (2017a). Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. Retrieved from http://arxiv.org/abs/1703.02837

(arXiv: 1703.02837) Abstract

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.

Export

BibTeX

@online{TeuckearXiv2017,
TITLE = {Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints},
AUTHOR = {Teucke, Andreas and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1703.02837},
EPRINT = {1703.02837},
EPRINTTYPE = {arXiv},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
ABSTRACT = {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.},
}

Endnote

%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

Teucke, A., & Weidenbach, C. (2017b). Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. In

*Automated Deduction -- CADE 26*. Gothenburg, Sweden: Springer. doi:10.1007/978-3-319-63046-5_13Export

BibTeX

@inproceedings{TeuckeCADE2017,
TITLE = {Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints},
AUTHOR = {Teucke, Andreas and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-319-63045-8},
DOI = {10.1007/978-3-319-63046-5_13},
PUBLISHER = {Springer},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
BOOKTITLE = {Automated Deduction -- CADE 26},
EDITOR = {de Moura, Leonardo},
PAGES = {202--219},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {10395},
ADDRESS = {Gothenburg, Sweden},
}

Endnote

%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

Voigt, M. (2017a). A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment. In

*32nd Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2017)*. Reykjavik, Iceland: ACM. doi:10.1109/LICS.2017.8005094Export

BibTeX

@inproceedings{VoigtLICS2017,
TITLE = {A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment},
AUTHOR = {Voigt, Marco},
LANGUAGE = {eng},
ISBN = {978-1-5090-3019-4},
DOI = {10.1109/LICS.2017.8005094},
PUBLISHER = {ACM},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
BOOKTITLE = {32nd Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2017)},
PAGES = {1--12},
ADDRESS = {Reykjavik, Iceland},
}

Endnote

%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

Voigt, M. (2017b). A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment. Retrieved from http://arxiv.org/abs/1704.02145

(arXiv: 1704.02145) Abstract

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.

Export

BibTeX

@online{VoigtLICS2017ArxivFullPaper,
TITLE = {A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment},
AUTHOR = {Voigt, Marco},
URL = {http://arxiv.org/abs/1704.02145},
EPRINT = {1704.02145},
EPRINTTYPE = {arXiv},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
ABSTRACT = {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.},
}

Endnote

%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

Voigt, M. (2017c). The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable. In

*Frontiers of Combining Systems (FroCoS 2017)*. Brasília, Brazil: Springer. doi:10.1007/978-3-319-66167-4_14Export

BibTeX

@inproceedings{VoigtFroCoS2017,
TITLE = {The {B}ernays--{S}ch{\"o}nfinkel--{R}amsey Fragment with Bounded Difference Constraints over the Reals Is Decidable},
AUTHOR = {Voigt, Marco},
LANGUAGE = {eng},
ISBN = {978-3-319-66166-7},
DOI = {10.1007/978-3-319-66167-4_14},
PUBLISHER = {Springer},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
BOOKTITLE = {Frontiers of Combining Systems (FroCoS 2017)},
EDITOR = {Dixon, Clare and Finger, Marcelo},
PAGES = {244--261},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {10483},
ADDRESS = {Bras{\'i}lia, Brazil},
}

Endnote

%0 Conference Proceedings
%A Voigt, Marco
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T The Bernays-Schö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í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

Voigt, M. (2017d). On Generalizing Decidable Standard Prefix Classes of First-Order Logic. Retrieved from http://arxiv.org/abs/1706.03949

(arXiv: 1706.03949) Abstract

Recently, the separated fragment (SF) of first-order logic has been
introduced. Its defining principle is that universally and existentially
quantified variables may not occur together in atoms. SF properly generalizes
both the Bernays-Sch\"onfinkel-Ramsey (BSR) fragment and the relational monadic
fragment. In this paper the restrictions on variable occurrences in SF
sentences are relaxed such that universally and existentially quantified
variables may occur together in the same atom under certain conditions. Still,
satisfiability can be decided. This result is established in two ways: firstly,
by an effective equivalence-preserving translation into the BSR fragment, and,
secondly, by a model-theoretic argument.
Slight modifications to the described concepts facilitate the definition of
other decidable classes of first-order sentences. The paper presents a second
fragment which is novel, has a decidable satisfiability problem, and properly
contains the Ackermann fragment and---once more---the relational monadic
fragment. The definition is again characterized by restrictions on the
occurrences of variables in atoms. More precisely, after certain
transformations, Skolemization yields only unary functions and constants, and
every atom contains at most one universally quantified variable. An effective
satisfiability-preserving translation into the monadic fragment is devised and
employed to prove decidability of the associated satisfiability problem.

Export

BibTeX

@online{Voigt_arXiv1706.03949,
TITLE = {On Generalizing Decidable Standard Prefix Classes of First-Order Logic},
AUTHOR = {Voigt, Marco},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1706.03949},
EPRINT = {1706.03949},
EPRINTTYPE = {arXiv},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
ABSTRACT = {Recently, the separated fragment (SF) of first-order logic has been introduced. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. SF properly generalizes both the Bernays-Sch\"onfinkel-Ramsey (BSR) fragment and the relational monadic fragment. In this paper the restrictions on variable occurrences in SF sentences are relaxed such that universally and existentially quantified variables may occur together in the same atom under certain conditions. Still, satisfiability can be decided. This result is established in two ways: firstly, by an effective equivalence-preserving translation into the BSR fragment, and, secondly, by a model-theoretic argument. Slight modifications to the described concepts facilitate the definition of other decidable classes of first-order sentences. The paper presents a second fragment which is novel, has a decidable satisfiability problem, and properly contains the Ackermann fragment and---once more---the relational monadic fragment. The definition is again characterized by restrictions on the occurrences of variables in atoms. More precisely, after certain transformations, Skolemization yields only unary functions and constants, and every atom contains at most one universally quantified variable. An effective satisfiability-preserving translation into the monadic fragment is devised and employed to prove decidability of the associated satisfiability problem.},
}

Endnote

%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
introduced. Its defining principle is that universally and existentially
quantified variables may not occur together in atoms. SF properly generalizes
both the Bernays-Sch\"onfinkel-Ramsey (BSR) fragment and the relational monadic
fragment. In this paper the restrictions on variable occurrences in SF
sentences are relaxed such that universally and existentially quantified
variables may occur together in the same atom under certain conditions. Still,
satisfiability can be decided. This result is established in two ways: firstly,
by an effective equivalence-preserving translation into the BSR fragment, and,
secondly, by a model-theoretic argument.
Slight modifications to the described concepts facilitate the definition of
other decidable classes of first-order sentences. The paper presents a second
fragment which is novel, has a decidable satisfiability problem, and properly
contains the Ackermann fragment and---once more---the relational monadic
fragment. The definition is again characterized by restrictions on the
occurrences of variables in atoms. More precisely, after certain
transformations, Skolemization yields only unary functions and constants, and
every atom contains at most one universally quantified variable. An effective
satisfiability-preserving translation into the monadic fragment is devised and
employed to prove decidability of the associated satisfiability problem.
%K Computer Science, Logic in Computer Science, cs.LO

Voigt, M. (2017e). The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable. Retrieved from http://arxiv.org/abs/1706.08504

(arXiv: 1706.08504) Abstract

First-order linear real arithmetic enriched with uninterpreted predicate
symbols yields an interesting modeling language. However, satisfiability of
such formulas is undecidable, even if we restrict the uninterpreted predicate
symbols to arity one. In order to find decidable fragments of this language, it
is necessary to restrict the expressiveness of the arithmetic part. One
possible path is to confine arithmetic expressions to difference constraints of
the form $x - y \mathrel{\#} c$, where $\#$ ranges over the standard relations
$<, \leq, =, \neq, \geq, >$ and $x,y$ are universally quantified. However, it
is known that combining difference constraints with uninterpreted predicate
symbols yields an undecidable satisfiability problem again. In this paper, it
is shown that satisfiability becomes decidable if we in addition bound the
ranges of universally quantified variables. As bounded intervals over the reals
still comprise infinitely many values, a trivial instantiation procedure is not
sufficient to solve the problem.

Export

BibTeX

@online{Voigt_arXIv1706.08504,
TITLE = {The {B}ernays--{S}ch{\"o}nfinkel--{R}amsey {Fragment with Bounded Difference Constraints over the Reals Is Decidable}},
AUTHOR = {Voigt, Marco},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1706.08504},
EPRINT = {1706.08504},
EPRINTTYPE = {arXiv},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
ABSTRACT = {First-order linear real arithmetic enriched with uninterpreted predicate symbols yields an interesting modeling language. However, satisfiability of such formulas is undecidable, even if we restrict the uninterpreted predicate symbols to arity one. In order to find decidable fragments of this language, it is necessary to restrict the expressiveness of the arithmetic part. One possible path is to confine arithmetic expressions to difference constraints of the form $x -- y \mathrel{\#} c$, where $\#$ ranges over the standard relations $<, \leq, =, \neq, \geq, >$ and $x,y$ are universally quantified. However, it is known that combining difference constraints with uninterpreted predicate symbols yields an undecidable satisfiability problem again. In this paper, it is shown that satisfiability becomes decidable if we in addition bound the ranges of universally quantified variables. As bounded intervals over the reals still comprise infinitely many values, a trivial instantiation procedure is not sufficient to solve the problem.},
}

Endnote

%0 Report
%A Voigt, Marco
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T The Bernays-Schö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
symbols yields an interesting modeling language. However, satisfiability of
such formulas is undecidable, even if we restrict the uninterpreted predicate
symbols to arity one. In order to find decidable fragments of this language, it
is necessary to restrict the expressiveness of the arithmetic part. One
possible path is to confine arithmetic expressions to difference constraints of
the form $x - y \mathrel{\#} c$, where $\#$ ranges over the standard relations
$<, \leq, =, \neq, \geq, >$ and $x,y$ are universally quantified. However, it
is known that combining difference constraints with uninterpreted predicate
symbols yields an undecidable satisfiability problem again. In this paper, it
is shown that satisfiability becomes decidable if we in addition bound the
ranges of universally quantified variables. As bounded intervals over the reals
still comprise infinitely many values, a trivial instantiation procedure is not
sufficient to solve the problem.
%K Computer Science, Logic in Computer Science, cs.LO

Voigt, M. (2017f). Towards Elimination of Second-Order Quantifiers in the Separated Fragment. In

*Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017)*. Dresden, Germany: CEUR-WS. Retrieved from urn:nbn:de:0074-2013-7Export

BibTeX

@inproceedings{Voigt_SOQE2017,
TITLE = {Towards Elimination of Second-Order Quantifiers in the Separated Fragment},
AUTHOR = {Voigt, Marco},
LANGUAGE = {eng},
URL = {urn:nbn:de:0074-2013-7},
PUBLISHER = {CEUR-WS},
YEAR = {2018},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017)},
EDITOR = {Koopmann, Patrick and Rudolph, Sebastian and Schmidt, Renate A. and Wernhard, Christoph},
PAGES = {67--81},
EID = {16},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {2013},
ADDRESS = {Dresden, Germany},
}

Endnote

%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

Wand, D. (2017).

*Superposition: Types and Induction*. Universität des Saarlandes, Saarbrücken. Retrieved from urn:nbn:de:bsz:291-scidok-69522Abstract

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.
However, they incur a significant overhead compared to pen-and-paper proofs.
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.
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.
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.
I have implemented the contributions in a tool called Pirate. The evaluations of both contributions show promising results.

Export

BibTeX

@phdthesis{wandphd2017,
TITLE = {Superposition: Types and Induction},
AUTHOR = {Wand, Daniel},
LANGUAGE = {eng},
URL = {urn:nbn:de:bsz:291-scidok-69522},
SCHOOL = {Universit{\"a}t des Saarlandes},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
DATE = {2017},
ABSTRACT = {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. However, they incur a significant overhead compared to pen-and-paper proofs. 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. 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. 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. I have implemented the contributions in a tool called Pirate. The evaluations of both contributions show promising results.},
}

Endnote

%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
%I Universität des Saarlandes
%C Saarbrü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.
However, they incur a significant overhead compared to pen-and-paper proofs.
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.
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.
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.
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

Weidenbach, C. (2017). Do Portfolio Solvers Harm? In

*ARCADE 2017*. Gothenburg, Sweden. doi:10.29007/vpxmExport

BibTeX

@inproceedings{Weidenbach_ARCADE2017,
TITLE = {Do Portfolio Solvers Harm?},
AUTHOR = {Weidenbach, Christoph},
LANGUAGE = {eng},
DOI = {10.29007/vpxm},
YEAR = {2017},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {ARCADE 2017},
EDITOR = {Reger, Giles and Traytel, Dmitriy},
PAGES = {76--81},
SERIES = {EPiC Series in Computing},
VOLUME = {51},
ADDRESS = {Gothenburg, Sweden},
}

Endnote

%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