The Year Before Last

Alagi, G., & Weidenbach, C. (2015a). NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment. In Frontiers of Combining Systems (FroCoS 2015). Wrocław, Poland: Springer. doi:10.1007/978-3-319-24246-0_5
Export
BibTeX
@inproceedings{AlagiFroCoS2015, TITLE = {{NRCL} -- A Model Building Approach to the {Bernays}-{S}ch{\"o}nfinkel Fragment}, AUTHOR = {Alagi, G{\'a}bor and Weidenbach, Christoph}, LANGUAGE = {eng}, ISBN = {978-3-319-2424}, DOI = {10.1007/978-3-319-24246-0_5}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Frontiers of Combining Systems (FroCoS 2015)}, EDITOR = {Lutz, Carsten and Ranise, Silvio}, PAGES = {69--84}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {9322}, ADDRESS = {Wroc{\l}aw, Poland}, }
Endnote
%0 Conference Proceedings %A Alagi, Gábor %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0028-8EFA-E %R 10.1007/978-3-319-24246-0_5 %D 2015 %B 10th International Symposium on Frontiers of Combining Systems %Z date of event: 2015-09-21 - 2015-09-24 %C Wrocław, Poland %B Frontiers of Combining Systems %E Lutz, Carsten; Ranise, Silvio %P 69 - 84 %I Springer %@ 978-3-319-2424 %B Lecture Notes in Artificial Intelligence %N 9322
Alagi, G., & Weidenbach, C. (2015b). NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment. Retrieved from http://arxiv.org/abs/1502.05501
(arXiv: 1502.05501)
Abstract
We combine key ideas from first-order superposition and propositional CDCL to create the new calculus NRCL deciding the Bernays-Sch\"onfinkel fragment. It inherits the abstract redundancy criterion and the monotone model operator from superposition. CDCL adds to NRCL the dynamic, conflict-driven search for an atom ordering inducing a model. As a result, in NRCL a false clause can be effectively found modulo the current model assumption. It guides the derivation of a first-order ordered resolvent that is never redundant. Similar to 1UIP-learning in CDCL, the learned resolvent induces backtracking and via propagation blocks the previous conflict state for the rest of the search. Since learned clauses are never redundant, only finitely many can be generated by NRCL on the Bernays-Sch\"onfinkel fragment, which provides a nice argument for termination.
Export
BibTeX
@online{DBLP:journals/corr/AlagiW15, TITLE = {{NRCL} -- A Model Building Approach to the {B}ernays-{S}ch{\"o}nfinkel Fragment}, AUTHOR = {Alagi, G{\'a}bor and Weidenbach, Christoph}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1502.05501}, EPRINT = {1502.05501}, EPRINTTYPE = {arXiv}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, ABSTRACT = {We combine key ideas from first-order superposition and propositional CDCL to create the new calculus NRCL deciding the Bernays-Sch\"onfinkel fragment. It inherits the abstract redundancy criterion and the monotone model operator from superposition. CDCL adds to NRCL the dynamic, conflict-driven search for an atom ordering inducing a model. As a result, in NRCL a false clause can be effectively found modulo the current model assumption. It guides the derivation of a first-order ordered resolvent that is never redundant. Similar to 1UIP-learning in CDCL, the learned resolvent induces backtracking and via propagation blocks the previous conflict state for the rest of the search. Since learned clauses are never redundant, only finitely many can be generated by NRCL on the Bernays-Sch\"onfinkel fragment, which provides a nice argument for termination.}, }
Endnote
%0 Report %A Alagi, Gábor %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0025-B02B-F %U http://arxiv.org/abs/1502.05501 %D 2015 %8 19.02.2015 %X We combine key ideas from first-order superposition and propositional CDCL to create the new calculus NRCL deciding the Bernays-Sch\"onfinkel fragment. It inherits the abstract redundancy criterion and the monotone model operator from superposition. CDCL adds to NRCL the dynamic, conflict-driven search for an atom ordering inducing a model. As a result, in NRCL a false clause can be effectively found modulo the current model assumption. It guides the derivation of a first-order ordered resolvent that is never redundant. Similar to 1UIP-learning in CDCL, the learned resolvent induces backtracking and via propagation blocks the previous conflict state for the rest of the search. Since learned clauses are never redundant, only finitely many can be generated by NRCL on the Bernays-Sch\"onfinkel fragment, which provides a nice argument for termination. %K Computer Science, Logic in Computer Science, cs.LO
Barkatou, M. A., Jaroschek, M., & Maddah, S. S. (2015). Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings. Retrieved from http://arxiv.org/abs/1511.00180
(arXiv: 1511.00180)
Abstract
In this paper, we present an algorithm for computing a fundamental matrix of formal solutions of completely integrable Pfaffian systems with normal crossings in several variables. This algorithm is a generalization of a method developed for the bivariate case based on a combination of several reduction techniques and is implemented in the computer algebra system Maple.
Export
BibTeX
@online{DBLP:journals/corr/BarkatouJM15, TITLE = {Formal Solutions of Completely Integrable {Pfaffian} Systems With Normal Crossings}, AUTHOR = {Barkatou, Moulay A. and Jaroschek, Maximilian and Maddah, Suzy S.}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1511.00180}, EPRINT = {1511.00180}, EPRINTTYPE = {arXiv}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, ABSTRACT = {In this paper, we present an algorithm for computing a fundamental matrix of formal solutions of completely integrable Pfaffian systems with normal crossings in several variables. This algorithm is a generalization of a method developed for the bivariate case based on a combination of several reduction techniques and is implemented in the computer algebra system Maple.}, }
Endnote
%0 Report %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-0029-6635-6 %U http://arxiv.org/abs/1511.00180 %D 2015 %X In this paper, we present an algorithm for computing a fundamental matrix of formal solutions of completely integrable Pfaffian systems with normal crossings in several variables. This algorithm is a generalization of a method developed for the bivariate case based on a combination of several reduction techniques and is implemented in the computer algebra system Maple. %K Computer Science, Symbolic Computation, cs.SC
Baumgartner, P., Bax, J., & Waldmann, U. (2015). Beagle -- A Hierarchic Superposition Theorem Prover. In Automated Deduction -- CADE-25. Berlin, Germany: Springer. doi:10.1007/978-3-319-21401-6_25
Export
BibTeX
@inproceedings{BaumgartnerCADE2015, TITLE = {Beagle -- A Hierarchic Superposition Theorem Prover}, AUTHOR = {Baumgartner, Peter and Bax, Joshua and Waldmann, Uwe}, LANGUAGE = {eng}, ISBN = {978-3-319-21400-9}, DOI = {10.1007/978-3-319-21401-6_25}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Automated Deduction -- CADE-25}, EDITOR = {Felty, Amy P. and Middeldorp, Aart}, PAGES = {367--377}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {9195}, ADDRESS = {Berlin, Germany}, }
Endnote
%0 Conference Proceedings %A Baumgartner, Peter %A Bax, Joshua %A Waldmann, Uwe %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Beagle -- A Hierarchic Superposition Theorem Prover : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-07D8-3 %R 10.1007/978-3-319-21401-6_25 %D 2015 %B 25th International Conference on Automated Deduction %Z date of event: 2015-08-01 - 2015-08-07 %C Berlin, Germany %B Automated Deduction -- CADE-25 %E Felty, Amy P.; Middeldorp, Aart %P 367 - 377 %I Springer %@ 978-3-319-21400-9 %B Lecture Notes in Artificial Intelligence %N 9195
Blanchette, J. C., Popescu, A., & Traytel, D. (2015a). Foundational Extensible Corecursion: A Proof Assistant Perspective. In ACM SIGPLAN Notices (Proc. ICFP 2015) (Vol. 50). Vancouver, BC, Canada: ACM. doi:10.1145/2784731.2784732
Export
BibTeX
@inproceedings{DBLP:conf/icfp/Blanchette0T15, TITLE = {Foundational Extensible Corecursion: A Proof Assistant Perspective}, AUTHOR = {Blanchette, Jasmin Christian and Popescu, Andrei and Traytel, Dmitriy}, LANGUAGE = {eng}, ISSN = {0362-1340}, ISBN = {978-1-4503-3669-7}, DOI = {10.1145/2784731.2784732}, PUBLISHER = {ACM}, PUBLISHER = {ACM Press}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015)}, PAGES = {192--204}, JOURNAL = {ACM SIGPLAN Notices (Proc. ICFP)}, VOLUME = {50}, ISSUE = {9}, ADDRESS = {Vancouver, BC, Canada}, }
Endnote
%0 Conference Proceedings %A Blanchette, Jasmin Christian %A Popescu, Andrei %A Traytel, Dmitriy %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Foundational Extensible Corecursion: A Proof Assistant Perspective : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-5B18-E %R 10.1145/2784731.2784732 %D 2015 %B 20th ACM SIGPLAN International Conference on Functional Programming %Z date of event: 2015-09-01 - 2015-09-03 %C Vancouver, BC, Canada %B Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming %P 192 - 204 %I ACM %@ 978-1-4503-3669-7 %J ACM SIGPLAN Notices %V 50 %N 9 %I ACM Press %@ false %U http://doi.acm.org/10.1145/2784731.2784732
Blanchette, J. C., Popescu, A., & Traytel, D. (2015b). Foundational Extensible Corecursion. Retrieved from http://arxiv.org/abs/1501.05425
(arXiv: 1501.05425)
Abstract
This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls under well-behaved operations, including constructors. Corecursive functions that are well behaved can be registered as such, thereby increasing the corecursor's expressiveness. The metatheory is formalized in the Isabelle proof assistant and forms the core of a prototype tool. The corecursor is derived from first principles, without requiring new axioms or extensions of the logic.
Export
BibTeX
@online{BlanchetteFoundArxiv15, TITLE = {Foundational Extensible Corecursion}, AUTHOR = {Blanchette, Jasmin Christian and Popescu, Andrei and Traytel, Dmitriy}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1501.05425}, EPRINT = {1501.05425}, EPRINTTYPE = {arXiv}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, ABSTRACT = {This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls under well-behaved operations, including constructors. Corecursive functions that are well behaved can be registered as such, thereby increasing the corecursor's expressiveness. The metatheory is formalized in the Isabelle proof assistant and forms the core of a prototype tool. The corecursor is derived from first principles, without requiring new axioms or extensions of the logic.}, }
Endnote
%0 Report %A Blanchette, Jasmin Christian %A Popescu, Andrei %A Traytel, Dmitriy %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Foundational Extensible Corecursion : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-5B30-5 %U http://arxiv.org/abs/1501.05425 %D 2015 %8 22.01.2015 %X This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls under well-behaved operations, including constructors. Corecursive functions that are well behaved can be registered as such, thereby increasing the corecursor's expressiveness. The metatheory is formalized in the Isabelle proof assistant and forms the core of a prototype tool. The corecursor is derived from first principles, without requiring new axioms or extensions of the logic. %K Computer Science, Programming Languages, cs.PL
Blanchette, J. C., & Kosmatov, N. (Eds.). (2015). Tests and Proofs. Presented at the 9th International Conference on Tests & Proofs, L’Aquila, Italy: Springer. doi:10.1007/978-3-319-21215-9
Export
BibTeX
@proceedings{DBLP:conf/tap/2015, TITLE = {Tests and Proofs (TAP 2015)}, EDITOR = {Blanchette, Jasmin Christian and Kosmatov, Nikolai}, LANGUAGE = {eng}, ISSN = {0302-9743}, ISBN = {978-3-319-21214-2}, DOI = {10.1007/978-3-319-21215-9}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {9154}, ADDRESS = {L'Aquila, Italy}, }
Endnote
%0 Conference Proceedings %E Blanchette, Jasmin Christian %E Kosmatov, Nikolai %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Tests and Proofs : 9th International Conference, TAP 2015, Held as Part of STAF 2015 ; L'Aquila, Italy, July 22-24, 2015 ; Proceedings %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-5B21-7 %@ 978-3-319-21214-2 %R 10.1007/978-3-319-21215-9 %I Springer %D 2015 %B 9th International Conference on Tests & Proofs %Z date of event: 2015-07-22 - 2015-07-24 %D 2015 %C L'Aquila, Italy %S Lecture Notes in Computer Science %V 9154 %@ false
Blanchette, J. C., Haslbeck, M., Matichuk, D., & Nipkow, T. (2015). Mining the Archive of Formal Proofs. In Intelligent Computer Mathematics (CICM 2015). Washington, DC, USA: Springer. doi:10.1007/978-3-319-20615-8_1
Export
BibTeX
@inproceedings{BlanchetteCIKM2015, TITLE = {Mining the Archive of Formal Proofs}, AUTHOR = {Blanchette, Jasmin Christian and Haslbeck, Maximilian and Matichuk, Daniel and Nipkow, Tobias}, LANGUAGE = {eng}, ISBN = {978-3-319-20614-1}, DOI = {10.1007/978-3-319-20615-8_1}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Intelligent Computer Mathematics (CICM 2015)}, EDITOR = {Kerber, Manfred and Carette, Jacques and Kaliszyk, Cezary and Rabe, Florian and Sorge, Volker}, PAGES = {3--17}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {9150}, ADDRESS = {Washington, DC, USA}, }
Endnote
%0 Conference Proceedings %A Blanchette, Jasmin Christian %A Haslbeck, Maximilian %A Matichuk, Daniel %A Nipkow, Tobias %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations %T Mining the Archive of Formal Proofs : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0028-5D84-A %R 10.1007/978-3-319-20615-8_1 %D 2015 %B International Conference on Intelligent Computer Mathematics %Z date of event: 2015-07-13 - 2015-07-17 %C Washington, DC, USA %B Intelligent Computer Mathematics %E Kerber, Manfred; Carette, Jacques; Kaliszyk, Cezary; Rabe, Florian; Sorge, Volker %P 3 - 17 %I Springer %@ 978-3-319-20614-1 %B Lecture Notes in Artificial Intelligence %N 9150
Blanchette, J. C., Popescu, A., & Traytel, D. (2015c). Witnessing (Co)datatypes. In Programming Languages and Systems (ESOP 2015). London, UK: Springer. doi:10.1007/978-3-662-46669-8_15
Export
BibTeX
@inproceedings{BlanchetteESOP2015, TITLE = {Witnessing (Co)datatypes}, AUTHOR = {Blanchette, Jasmin Christian and Popescu, Andrei and Traytel, Dmitriy}, LANGUAGE = {eng}, ISBN = {978-3-662-46668-1}, DOI = {10.1007/978-3-662-46669-8_15}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Programming Languages and Systems (ESOP 2015)}, EDITOR = {Vitek, Jan}, PAGES = {359--382}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {9032}, ADDRESS = {London, UK}, }
Endnote
%0 Conference Proceedings %A Blanchette, Jasmin Christian %A Popescu, Andrei %A Traytel, Dmitriy %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Witnessing (Co)datatypes : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0028-E142-C %R 10.1007/978-3-662-46669-8_15 %D 2015 %B 24th European Symposium on Programming %Z date of event: 2015-04-11 - 2015-04-18 %C London, UK %B Programming Languages and Systems %E Vitek, Jan %P 359 - 382 %I Springer %@ 978-3-662-46668-1 %B Lecture Notes in Computer Science %N 9032
Bromberger, M., Sturm, T., & Weidenbach, C. (2015a). Linear Integer Arithmetic Revisited. In Automated Deduction -- CADE-25. Berlin, Germany: Springer. doi:10.1007/978-3-319-21401-6_42
Export
BibTeX
@inproceedings{BrombergerCADE2015, TITLE = {Linear Integer Arithmetic Revisited}, AUTHOR = {Bromberger, Martin and Sturm, Thomas and Weidenbach, Christoph}, LANGUAGE = {eng}, ISBN = {978-3-319-21400-9}, DOI = {10.1007/978-3-319-21401-6_42}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Automated Deduction -- CADE-25}, EDITOR = {Felty, Amy P. and Middeldorp, Aart}, PAGES = {623--637}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {9195}, ADDRESS = {Berlin, Germany}, }
Endnote
%0 Conference Proceedings %A Bromberger, Martin %A Sturm, Thomas %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 Linear Integer Arithmetic Revisited : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0028-8EE6-9 %R 10.1007/978-3-319-21401-6_42 %D 2015 %B 25th International Conference on Automated Deduction %Z date of event: 2015-08-01 - 2015-08-07 %C Berlin, Germany %B Automated Deduction -- CADE-25 %E Felty, Amy P.; Middeldorp, Aart %P 623 - 637 %I Springer %@ 978-3-319-21400-9 %B Lecture Notes in Artificial Intelligence %N 9195
Bromberger, M., Sturm, T., & Weidenbach, C. (2015b). Linear Integer Arithmetic Revisited. Retrieved from http://arxiv.org/abs/1503.02948
(arXiv: 1503.02948)
Abstract
We consider feasibility of linear integer programs in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer programs is decidable, many state-of-the-art solvers neglect termination in favor of efficiency. It is challenging to design a solver that is both terminating and practically efficient. Recent work by Jovanovic and de Moura constitutes an important step into this direction. Their algorithm CUTSAT is sound, but does not terminate, in general. In this paper we extend their CUTSAT algorithm by refined inference rules, a new type of conflicting core, and a dedicated rule application strategy. This leads to our algorithm CUTSAT++, which guarantees termination.
Export
BibTeX
@online{BrombergerSturmWeidenbacharXiv2015, TITLE = {Linear Integer Arithmetic Revisited}, AUTHOR = {Bromberger, Martin and Sturm, Thomas and Weidenbach, Christoph}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1503.02948}, EPRINT = {1503.02948}, EPRINTTYPE = {arXiv}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, ABSTRACT = {We consider feasibility of linear integer programs in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer programs is decidable, many state-of-the-art solvers neglect termination in favor of efficiency. It is challenging to design a solver that is both terminating and practically efficient. Recent work by Jovanovic and de Moura constitutes an important step into this direction. Their algorithm CUTSAT is sound, but does not terminate, in general. In this paper we extend their CUTSAT algorithm by refined inference rules, a new type of conflicting core, and a dedicated rule application strategy. This leads to our algorithm CUTSAT++, which guarantees termination.}, }
Endnote
%0 Report %A Bromberger, Martin %A Sturm, Thomas %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 Linear Integer Arithmetic Revisited : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0025-6937-4 %U http://arxiv.org/abs/1503.02948 %D 2015 %8 10.03.2015 %X We consider feasibility of linear integer programs in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer programs is decidable, many state-of-the-art solvers neglect termination in favor of efficiency. It is challenging to design a solver that is both terminating and practically efficient. Recent work by Jovanovic and de Moura constitutes an important step into this direction. Their algorithm CUTSAT is sound, but does not terminate, in general. In this paper we extend their CUTSAT algorithm by refined inference rules, a new type of conflicting core, and a dedicated rule application strategy. This leads to our algorithm CUTSAT++, which guarantees termination. %K Computer Science, Logic in Computer Science, cs.LO
Brown, C. W., & Košta, M. (2015). Constructing a Single Cell in Cylindrical Algebraic Decomposition. Journal of Symbolic Computation, 70. doi:10.1016/j.jsc.2014.09.024
Export
BibTeX
@article{BrownKosta:2014a, TITLE = {Constructing a Single Cell in Cylindrical Algebraic Decomposition}, AUTHOR = {Brown, Christopher W. and Ko{\v s}ta, Marek}, LANGUAGE = {eng}, ISSN = {0747-7171}, DOI = {10.1016/j.jsc.2014.09.024}, PUBLISHER = {Academic Press}, ADDRESS = {London}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, JOURNAL = {Journal of Symbolic Computation}, VOLUME = {70}, PAGES = {14--48}, }
Endnote
%0 Journal Article %A Brown, Christopher W. %A Košta, Marek %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Constructing a Single Cell in Cylindrical Algebraic Decomposition : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0024-920D-7 %R 10.1016/j.jsc.2014.09.024 %7 2015 %D 2015 %J Journal of Symbolic Computation %V 70 %& 14 %P 14 - 48 %I Academic Press %C London %@ false
Damm, W., Horbach, M., & Sofronie-Stokkermans, V. (2015a). Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata. In Frontiers of Combining Systems (FroCoS 2015). Wrocław, Poland: Springer. doi:10.1007/978-3-319-24246-0_12
Export
BibTeX
@inproceedings{DammFroCoS2015, TITLE = {Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata}, AUTHOR = {Damm, Werner and Horbach, Matthias and Sofronie-Stokkermans, Viorica}, LANGUAGE = {eng}, ISBN = {978-3-319-2424}, DOI = {10.1007/978-3-319-24246-0_12}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Frontiers of Combining Systems (FroCoS 2015)}, EDITOR = {Lutz, Carsten and Ranise, Silvio}, PAGES = {186--202}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {9322}, ADDRESS = {Wroc{\l}aw, Poland}, }
Endnote
%0 Conference Proceedings %A Damm, Werner %A Horbach, Matthias %A Sofronie-Stokkermans, Viorica %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-474D-8 %R 10.1007/978-3-319-24246-0_12 %D 2015 %B 10th International Symposium on Frontiers of Combining Systems %Z date of event: 2015-09-21 - 2015-09-24 %C Wrocław, Poland %B Frontiers of Combining Systems %E Lutz, Carsten; Ranise, Silvio %P 186 - 202 %I Springer %@ 978-3-319-2424 %B Lecture Notes in Artificial Intelligence %N 9322
Damm, W., Horbach, M., & Sofronie-Stokkermans, V. (2015b). Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata (No. ATR111). SFB/TR 14 AVACS.
Export
BibTeX
@techreport{atr111, TITLE = {Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata}, AUTHOR = {Damm, Werner and Horbach, Matthias and Sofronie-Stokkermans, Viorica}, LANGUAGE = {eng}, ISSN = {1860-9821}, NUMBER = {ATR111}, INSTITUTION = {SFB/TR 14 AVACS}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, TYPE = {AVACS Technical Report}, VOLUME = {111}, }
Endnote
%0 Report %A Damm, Werner %A Horbach, Matthias %A Sofronie-Stokkermans, Viorica %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002A-0805-6 %Y SFB/TR 14 AVACS %D 2015 %P 52 p. %B AVACS Technical Report %N 111 %@ false
Errami, H., Eiswirth, M., Grigoriev, D., Seiler, W. M., Sturm, T., & Weber, A. (2015). Detection of Hopf Bifurcations in Chemical Reaction Networks Using Convex Coordinates. Journal of Computational Physics, 291. doi:10.1016/j.jcp.2015.02.050
Export
BibTeX
@article{ErramiEiswirth:15a, TITLE = {Detection of {Hopf} Bifurcations in Chemical Reaction Networks Using Convex Coordinates}, AUTHOR = {Errami, Hassan and Eiswirth, Markus and Grigoriev, Dima and Seiler, Werner M. and Sturm, Thomas and Weber, Andreas}, LANGUAGE = {eng}, ISSN = {0021-9991}, DOI = {10.1016/j.jcp.2015.02.050}, PUBLISHER = {Elsevier}, ADDRESS = {Amsterdam}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, JOURNAL = {Journal of Computational Physics}, VOLUME = {291}, PAGES = {279--302}, }
Endnote
%0 Journal Article %A Errami, Hassan %A Eiswirth, Markus %A Grigoriev, Dima %A Seiler, Werner M. %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 Detection of Hopf Bifurcations in Chemical Reaction Networks Using Convex Coordinates : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0024-E260-7 %R 10.1016/j.jcp.2015.02.050 %7 2015-03-16 %D 2015 %J Journal of Computational Physics %V 291 %& 279 %P 279 - 302 %I Elsevier %C Amsterdam %@ false
Fontaine, P., Sturm, T., & Waldmann, U. (2015). Foreword to the Special Focus on Constraints and Combinations. Mathematics in Computer Science, 9(3). doi:10.1007/s11786-015-0239-8
Export
BibTeX
@article{DBLP:journals/mics/FontaineSW15, TITLE = {Foreword to the Special Focus on Constraints and Combinations}, AUTHOR = {Fontaine, Pascal and Sturm, Thomas and Waldmann, Uwe}, LANGUAGE = {eng}, ISSN = {1661-8270}, DOI = {10.1007/s11786-015-0239-8}, PUBLISHER = {Birkh{\"a}user}, ADDRESS = {Basel}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, JOURNAL = {Mathematics in Computer Science}, VOLUME = {9}, NUMBER = {3}, PAGES = {265--265}, }
Endnote
%0 Journal Article %A Fontaine, Pascal %A Sturm, Thomas %A Waldmann, Uwe %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Foreword to the Special Focus on Constraints and Combinations : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-661F-9 %R 10.1007/s11786-015-0239-8 %7 2015 %D 2015 %J Mathematics in Computer Science %V 9 %N 3 %& 265 %P 265 - 265 %I Birkhäuser %C Basel %@ false
Hagemann, W. (2015). Symbolic Orthogonal Projections: A New Polyhedral Representation for Reachability Analysis of Hybrid Systems. Universität des Saarlandes, Saarbrücken.
Export
BibTeX
@phdthesis{HagemannPhd15, TITLE = {Symbolic Orthogonal Projections: A New Polyhedral Representation for Reachability Analysis of Hybrid Systems}, AUTHOR = {Hagemann, Willem}, LANGUAGE = {eng}, SCHOOL = {Universit{\"a}t des Saarlandes}, ADDRESS = {Saarbr{\"u}cken}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, }
Endnote
%0 Thesis %A Hagemann, Willem %Y Weidenbach, Christoph %A referee: Fränzle, Martin %+ 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 Symbolic Orthogonal Projections: A New Polyhedral Representation for Reachability Analysis of Hybrid Systems : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-26AA-2 %I Universität des Saarlandes %C Saarbrücken %D 2015 %P XIII, 94 p. %V phd %9 phd %U http://scidok.sulb.uni-saarland.de/volltexte/2015/6304/http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=de
Hoeltgen, L., Mainberger, M., Hoffmann, S., Weickert, J., Tang, C. H., Setzer, S., … Doerr, B. (2015). Optimising Spatial and Tonal Data for PDE-based Inpainting. Retrieved from http://arxiv.org/abs/1506.04566
(arXiv: 1506.04566)
Abstract
Some recent methods for lossy signal and image compression store only a few selected pixels and fill in the missing structures by inpainting with a partial differential equation (PDE). Suitable operators include the Laplacian, the biharmonic operator, and edge-enhancing anisotropic diffusion (EED). The quality of such approaches depends substantially on the selection of the data that is kept. Optimising this data in the domain and codomain gives rise to challenging mathematical problems that shall be addressed in our work. In the 1D case, we prove results that provide insights into the difficulty of this problem, and we give evidence that a splitting into spatial and tonal (i.e. function value) optimisation does hardly deteriorate the results. In the 2D setting, we present generic algorithms that achieve a high reconstruction quality even if the specified data is very sparse. To optimise the spatial data, we use a probabilistic sparsification, followed by a nonlocal pixel exchange that avoids getting trapped in bad local optima. After this spatial optimisation we perform a tonal optimisation that modifies the function values in order to reduce the global reconstruction error. For homogeneous diffusion inpainting, this comes down to a least squares problem for which we prove that it has a unique solution. We demonstrate that it can be found efficiently with a gradient descent approach that is accelerated with fast explicit diffusion (FED) cycles. Our framework allows to specify the desired density of the inpainting mask a priori. Moreover, is more generic than other data optimisation approaches for the sparse inpainting problem, since it can also be extended to nonlinear inpainting operators such as EED. This is exploited to achieve reconstructions with state-of-the-art quality. We also give an extensive literature survey on PDE-based image compression methods.
Export
BibTeX
@online{DBLP:journals/corr/HoeltgenMHWTSJN15, TITLE = {Optimising Spatial and Tonal Data for {PDE}-based Inpainting}, AUTHOR = {Hoeltgen, Laurent and Mainberger, Markus and Hoffmann, Sebastian and Weickert, Joachim and Tang, Ching Hoo and Setzer, Simon and Johannsen, Daniel and Neumann, Frank and Doerr, Benjamin}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1506.04566}, EPRINT = {1506.04566}, EPRINTTYPE = {arXiv}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, ABSTRACT = {Some recent methods for lossy signal and image compression store only a few selected pixels and fill in the missing structures by inpainting with a partial differential equation (PDE). Suitable operators include the Laplacian, the biharmonic operator, and edge-enhancing anisotropic diffusion (EED). The quality of such approaches depends substantially on the selection of the data that is kept. Optimising this data in the domain and codomain gives rise to challenging mathematical problems that shall be addressed in our work. In the 1D case, we prove results that provide insights into the difficulty of this problem, and we give evidence that a splitting into spatial and tonal (i.e. function value) optimisation does hardly deteriorate the results. In the 2D setting, we present generic algorithms that achieve a high reconstruction quality even if the specified data is very sparse. To optimise the spatial data, we use a probabilistic sparsification, followed by a nonlocal pixel exchange that avoids getting trapped in bad local optima. After this spatial optimisation we perform a tonal optimisation that modifies the function values in order to reduce the global reconstruction error. For homogeneous diffusion inpainting, this comes down to a least squares problem for which we prove that it has a unique solution. We demonstrate that it can be found efficiently with a gradient descent approach that is accelerated with fast explicit diffusion (FED) cycles. Our framework allows to specify the desired density of the inpainting mask a priori. Moreover, is more generic than other data optimisation approaches for the sparse inpainting problem, since it can also be extended to nonlinear inpainting operators such as EED. This is exploited to achieve reconstructions with state-of-the-art quality. We also give an extensive literature survey on PDE-based image compression methods.}, }
Endnote
%0 Report %A Hoeltgen, Laurent %A Mainberger, Markus %A Hoffmann, Sebastian %A Weickert, Joachim %A Tang, Ching Hoo %A Setzer, Simon %A Johannsen, Daniel %A Neumann, Frank %A Doerr, Benjamin %+ External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations External Organizations %T Optimising Spatial and Tonal Data for PDE-based Inpainting : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-661C-F %U http://arxiv.org/abs/1506.04566 %D 2015 %X Some recent methods for lossy signal and image compression store only a few selected pixels and fill in the missing structures by inpainting with a partial differential equation (PDE). Suitable operators include the Laplacian, the biharmonic operator, and edge-enhancing anisotropic diffusion (EED). The quality of such approaches depends substantially on the selection of the data that is kept. Optimising this data in the domain and codomain gives rise to challenging mathematical problems that shall be addressed in our work. In the 1D case, we prove results that provide insights into the difficulty of this problem, and we give evidence that a splitting into spatial and tonal (i.e. function value) optimisation does hardly deteriorate the results. In the 2D setting, we present generic algorithms that achieve a high reconstruction quality even if the specified data is very sparse. To optimise the spatial data, we use a probabilistic sparsification, followed by a nonlocal pixel exchange that avoids getting trapped in bad local optima. After this spatial optimisation we perform a tonal optimisation that modifies the function values in order to reduce the global reconstruction error. For homogeneous diffusion inpainting, this comes down to a least squares problem for which we prove that it has a unique solution. We demonstrate that it can be found efficiently with a gradient descent approach that is accelerated with fast explicit diffusion (FED) cycles. Our framework allows to specify the desired density of the inpainting mask a priori. Moreover, is more generic than other data optimisation approaches for the sparse inpainting problem, since it can also be extended to nonlinear inpainting operators such as EED. This is exploited to achieve reconstructions with state-of-the-art quality. We also give an extensive literature survey on PDE-based image compression methods. %K Computer Science, Computer Vision and Pattern Recognition, cs.CV,Mathematics, Optimization and Control, math.OC,
Jaroschek, M., Dobal, P. F., & Fontaine, P. (2015). Adapting Real Quantifier Elimination Methods for Conflict Set Computation. In Frontiers of Combining Systems (FroCoS 2015). Wrocław, Poland: Springer. doi:10.1007/978-3-319-24246-0_10
Export
BibTeX
@inproceedings{JaroschekFroCoS2015, TITLE = {Adapting Real Quantifier Elimination Methods for Conflict Set Computation}, AUTHOR = {Jaroschek, Maximilian and Dobal, Pablo Federico and Fontaine, Pascal}, LANGUAGE = {eng}, ISBN = {978-3-319-2424}, DOI = {10.1007/978-3-319-24246-0_10}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Frontiers of Combining Systems (FroCoS 2015)}, EDITOR = {Lutz, Carsten and Ranise, Silvio}, PAGES = {151--166}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {9322}, ADDRESS = {Wroc{\l}aw, Poland}, }
Endnote
%0 Conference Proceedings %A Jaroschek, Maximilian %A Dobal, Pablo Federico %A Fontaine, Pascal %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Adapting Real Quantifier Elimination Methods for Conflict Set Computation : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-4794-8 %R 10.1007/978-3-319-24246-0_10 %D 2015 %B 10th International Symposium on Frontiers of Combining Systems %Z date of event: 2015-09-21 - 2015-09-24 %C Wrocław, Poland %B Frontiers of Combining Systems %E Lutz, Carsten; Ranise, Silvio %P 151 - 166 %I Springer %@ 978-3-319-2424 %B Lecture Notes in Artificial Intelligence %N 9322
Junk, C., Rößger, R., Rock, G., Theis, K., Weidenbach, C., & Wischnewski, P. (2015). Model-Based Variant Management with v.control. In Transdisciplinary Lifecycle Analysis of Systems (ISPE CE 2015). Delft, The Netherlands: IOS Press. doi:10.3233/978-1-61499-544-9-194
Export
BibTeX
@inproceedings{JunkISPECE2015, TITLE = {Model-Based Variant Management with v.control}, AUTHOR = {Junk, Christopher and R{\"o}{\ss}ger, Robert and Rock, Georg and Theis, Karsten and Weidenbach, Christoph and Wischnewski, Patrick}, LANGUAGE = {eng}, ISBN = {978-1-61499-543-2}, DOI = {10.3233/978-1-61499-544-9-194}, PUBLISHER = {IOS Press}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Transdisciplinary Lifecycle Analysis of Systems (ISPE CE 2015)}, EDITOR = {Curran, Richard and Wognum, Nel and Borsato, Milton and Stiepandic, Josip and Verhagen, Wim J. C.}, PAGES = {194--203}, SERIES = {Advances in Transdisciplinary Engineering}, VOLUME = {2}, ADDRESS = {Delft, The Netherlands}, }
Endnote
%0 Conference Proceedings %A Junk, Christopher %A Rößger, Robert %A Rock, Georg %A Theis, Karsten %A Weidenbach, Christoph %A Wischnewski, Patrick %+ External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Model-Based Variant Management with v.control : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0028-8F1F-5 %R 10.3233/978-1-61499-544-9-194 %D 2015 %B 22nd ISPE Inc. International Conference on Concurrent Engineering %Z date of event: 2015-07-20 - 2015-07-23 %C Delft, The Netherlands %B Transdisciplinary Lifecycle Analysis of Systems %E Curran, Richard; Wognum, Nel; Borsato, Milton; Stiepandic, Josip; Verhagen, Wim J. C. %P 194 - 203 %I IOS Press %@ 978-1-61499-543-2 %B Advances in Transdisciplinary Engineering %N 2
Kauers, M., Jaroschek, M., & Johannson, F. (2015). Ore Polynomials in Sage. In Computer Algebra and Polynomials. Berlin: Springer. doi:10.1007/978-3-319-15081-9_6
Export
BibTeX
@incollection{DBLP:series/lncs/KauersJJ15, TITLE = {Ore Polynomials in {Sage}}, AUTHOR = {Kauers, Manuel and Jaroschek, Maximilian and Johannson, Frederik}, LANGUAGE = {eng}, ISBN = {978-3-319-15080-2}, DOI = {10.1007/978-3-319-15081-9_6}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Computer Algebra and Polynomials}, EDITOR = {Gutierrez, Jaime and Schicho, Josef and Weiman, Martin}, PAGES = {105--125}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {8942}, }
Endnote
%0 Book Section %A Kauers, Manuel %A Jaroschek, Maximilian %A Johannson, Frederik %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Ore Polynomials in Sage : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-6633-A %R 10.1007/978-3-319-15081-9_6 %D 2015 %B Computer Algebra and Polynomials %E Gutierrez, Jaime; Schicho, Josef; Weiman, Martin %P 105 - 125 %I Springer %C Berlin %@ 978-3-319-15080-2 %S Lecture Notes in Computer Science %N 8942
Klein, F., & Zimmerman, M. (2015). What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead. In 24th EACSL Annual Conference on Computer Science Logic. Berlin, Germany: Wadern. doi:10.4230/LIPIcs.CSL.2015.519
Export
BibTeX
@inproceedings{KleinZ15, TITLE = {What are Strategies in Delay Games? {B}orel Determinacy for Games with Lookahead}, AUTHOR = {Klein, Felix and Zimmerman, Martin}, LANGUAGE = {eng}, ISSN = {1868-8969}, ISBN = {978-3-939897-90-3}, URL = {urn:nbn:de:0030-drops-54354}, DOI = {10.4230/LIPIcs.CSL.2015.519}, PUBLISHER = {Wadern}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, BOOKTITLE = {24th EACSL Annual Conference on Computer Science Logic}, EDITOR = {Kreutzer, Stephan}, PAGES = {519--533}, SERIES = {Leibniz International Proceedings in Informatics}, VOLUME = {41}, ADDRESS = {Berlin, Germany}, }
Endnote
%0 Conference Proceedings %A Klein, Felix %A Zimmerman, Martin %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-662F-5 %R 10.4230/LIPIcs.CSL.2015.519 %U urn:nbn:de:0030-drops-54354 %D 2015 %B 24th EACSL Annual Conference on Computer Science Logic %Z date of event: 2015-09-07 - 2015-09-10 %C Berlin, Germany %B 24th EACSL Annual Conference on Computer Science Logic %E Kreutzer, Stephan %P 519 - 533 %I Wadern %@ 978-3-939897-90-3 %B Leibniz International Proceedings in Informatics %N 41 %@ false %U http://drops.dagstuhl.de/doku/urheberrecht1.htmlhttp://drops.dagstuhl.de/opus/volltexte/2015/5435/
Klein, F., & Zimmermann, M. (2015). How Much Lookahead is Needed to Win Infinite Games? In Automata, Languages, and Programming (ICALP 2015). Kyoto, Japan: Springer. doi:10.1007/978-3-662-47666-6_36
Export
BibTeX
@inproceedings{Kleinlncs15, TITLE = {How Much Lookahead is Needed to Win Infinite Games?}, AUTHOR = {Klein, Felix and Zimmermann, Martin}, LANGUAGE = {eng}, ISBN = {978-3-662-47665-9}, DOI = {10.1007/978-3-662-47666-6_36}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Automata, Languages, and Programming (ICALP 2015)}, EDITOR = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi, Naoki and Speckmann, Bettina}, PAGES = {452--463}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {9135}, ADDRESS = {Kyoto, Japan}, }
Endnote
%0 Conference Proceedings %A Klein, Felix %A Zimmermann, Martin %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T How Much Lookahead is Needed to Win Infinite Games? : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-6621-1 %R 10.1007/978-3-662-47666-6_36 %D 2015 %B 42nd International Colloquium on Automata, Languages, and Programming %Z date of event: 2015-07-06 - 2015-07-10 %C Kyoto, Japan %B Automata, Languages, and Programming %E Halldórsson, Magnus M.; Iwama, Kazuo; Kobayashi, Naoki; Speckmann, Bettina %P 452 - 463 %I Springer %@ 978-3-662-47665-9 %B Lecture Notes in Computer Science %N 9135
Košta, M., & Sturm, T. (2015). A Generalized Framework for Virtual Substitution. Retrieved from http://arxiv.org/abs/1501.05826
(arXiv: 1501.05826)
Abstract
We generalize the framework of virtual substitution for real quantifier elimination to arbitrary but bounded degrees. We make explicit the representation of test points in elimination sets using roots of parametric univariate polynomials described by Thom codes. Our approach follows an early suggestion by Weispfenning, which has never been carried out explicitly. Inspired by virtual substitution for linear formulas, we show how to systematically construct elimination sets containing only test points representing lower bounds.
Export
BibTeX
@online{KostaSturmarXiv2015, TITLE = {A Generalized Framework for Virtual Substitution}, AUTHOR = {Ko{\v s}ta, Marek and Sturm, Thomas}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1501.05826}, EPRINT = {1501.05826}, EPRINTTYPE = {arXiv}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, ABSTRACT = {We generalize the framework of virtual substitution for real quantifier elimination to arbitrary but bounded degrees. We make explicit the representation of test points in elimination sets using roots of parametric univariate polynomials described by Thom codes. Our approach follows an early suggestion by Weispfenning, which has never been carried out explicitly. Inspired by virtual substitution for linear formulas, we show how to systematically construct elimination sets containing only test points representing lower bounds.}, }
Endnote
%0 Report %A Košta, Marek %A Sturm, Thomas %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T A Generalized Framework for Virtual Substitution : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0024-A3C1-0 %U http://arxiv.org/abs/1501.05826 %D 2015 %X We generalize the framework of virtual substitution for real quantifier elimination to arbitrary but bounded degrees. We make explicit the representation of test points in elimination sets using roots of parametric univariate polynomials described by Thom codes. Our approach follows an early suggestion by Weispfenning, which has never been carried out explicitly. Inspired by virtual substitution for linear formulas, we show how to systematically construct elimination sets containing only test points representing lower bounds. %K Computer Science, Symbolic Computation, cs.SC,Computer Science, Logic in Computer Science, cs.LO
Košta, M., Sturm, T., & Dolzmann, A. (2015). Better Answers to Real Questions. Retrieved from http://arxiv.org/abs/1501.05098
(arXiv: 1501.05098)
Abstract
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.
Export
BibTeX
@online{KostaarXiv2015, TITLE = {Better Answers to Real Questions}, AUTHOR = {Ko{\v s}ta, Marek and Sturm, Thomas and Dolzmann, Andreas}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1501.05098}, EPRINT = {1501.05098}, EPRINTTYPE = {arXiv}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, ABSTRACT = {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.}, }
Endnote
%0 Report %A Koš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-0024-9D8E-2 %U http://arxiv.org/abs/1501.05098 %D 2015 %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
Lamotte-Schubert, M. (2015). Automatic Authorization Analysis. Universität des Saarlandes, Saarbrücken. Retrieved from urn:nbn:de:bsz:291-scidok-62575
Export
BibTeX
@phdthesis{LamottePhd15, TITLE = {Automatic Authorization Analysis}, AUTHOR = {Lamotte-Schubert, Manuel}, LANGUAGE = {eng}, URL = {urn:nbn:de:bsz:291-scidok-62575}, SCHOOL = {Universit{\"a}t des Saarlandes}, ADDRESS = {Saarbr{\"u}cken}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, }
Endnote
%0 Thesis %A Lamotte-Schubert, Manuel %Y Weidenbach, Christoph %A referee: Baumgartner, Peter %+ 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 Automatic Authorization Analysis : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0028-FD0B-7 %U urn:nbn:de:bsz:291-scidok-62575 %I Universität des Saarlandes %C Saarbrücken %D 2015 %P 118 p. %V phd %9 phd %U http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=dehttp://scidok.sulb.uni-saarland.de/volltexte/2015/6257/
Reynolds, A., & Blanchette, J. C. (2015). A Decision Procedure for (Co)datatypes in SMT Solvers. In Automated Deduction -- CADE-25. Berlin, Germany: Springer. doi:10.1007/978-3-319-21401-6_13
Export
BibTeX
@inproceedings{ReynoldsCADE2015, TITLE = {A Decision Procedure for (Co)datatypes in {SMT} Solvers}, AUTHOR = {Reynolds, Andrew and Blanchette, Jasmin Christian}, LANGUAGE = {eng}, ISBN = {978-3-319-21400-9}, DOI = {10.1007/978-3-319-21401-6_13}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Automated Deduction -- CADE-25}, EDITOR = {Felty, Amy P. and Middeldorp, Aart}, PAGES = {197--213}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {9195}, ADDRESS = {Berlin, Germany}, }
Endnote
%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-0029-07D5-9 %R 10.1007/978-3-319-21401-6_13 %D 2015 %B 25th International Conference on Automated Deduction %Z date of event: 2015-08-01 - 2015-08-07 %C Berlin, Germany %B Automated Deduction -- CADE-25 %E Felty, Amy P.; Middeldorp, Aart %P 197 - 213 %I Springer %@ 978-3-319-21400-9 %B Lecture Notes in Artificial Intelligence %N 9195
Schmidt, R. A., & Waldmann, U. (2015a). Modal Tableau Systems with Blocking and Congruence Closure (No. uk-ac-man-scw:268816). Manchester: University of Manchester.
Export
BibTeX
@techreport{SchmidtTR2015, TITLE = {Modal Tableau Systems with Blocking and Congruence Closure}, AUTHOR = {Schmidt, Renate A. and Waldmann, Uwe}, LANGUAGE = {eng}, NUMBER = {uk-ac-man-scw:268816}, INSTITUTION = {University of Manchester}, ADDRESS = {Manchester}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, TYPE = {eScholar}, }
Endnote
%0 Report %A Schmidt, Renate A. %A Waldmann, Uwe %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Modal Tableau Systems with Blocking and Congruence Closure : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002A-08BC-A %Y University of Manchester %C Manchester %D 2015 %P 22 p. %B eScholar %U https://www.escholar.manchester.ac.uk/uk-ac-man-scw:268816https://www.research.manchester.ac.uk/portal/files/32297317/FULL_TEXT.PDF
Schmidt, R. A., & Waldmann, U. (2015b). Modal Tableau Systems with Blocking and Congruence Closure. In Automated Reasoning with Analytic Tableaux and Related Methods. Wrocław, Poland: Springer. doi:10.1007/978-3-319-24312-2_4
Export
BibTeX
@inproceedings{SchmidtTABLEAUX2015, TITLE = {Modal Tableau Systems with Blocking and Congruence Closure}, AUTHOR = {Schmidt, Renate A. and Waldmann, Uwe}, LANGUAGE = {eng}, ISBN = {978-3-319-24311-5}, DOI = {10.1007/978-3-319-24312-2_4}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Automated Reasoning with Analytic Tableaux and Related Methods}, EDITOR = {de Nivelle, Hans}, PAGES = {38--53}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {9323}, ADDRESS = {Wroc{\l}aw, Poland}, }
Endnote
%0 Conference Proceedings %A Schmidt, Renate A. %A Waldmann, Uwe %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Modal Tableau Systems with Blocking and Congruence Closure : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-4770-7 %R 10.1007/978-3-319-24312-2_4 %D 2015 %B 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods %Z date of event: 2015-09-21 - 2015-09-24 %C Wrocław, Poland %B Automated Reasoning with Analytic Tableaux and Related Methods %E de Nivelle, Hans %P 38 - 53 %I Springer %@ 978-3-319-24311-5 %B Lecture Notes in Artificial Intelligence %N 9323
Sofronie-Stokkermans, V. (2015). Hierarchical Reasoning in Local Theory Extensions and Applications. In SYNASC 2014. Timisoara, Romania: IEEE Computer Society. doi:10.1109/SYNASC.2014.13
Export
BibTeX
@inproceedings{sofronie-stokkermans-synasc2014, TITLE = {Hierarchical Reasoning in Local Theory Extensions and Applications}, AUTHOR = {Sofronie-Stokkermans, Viorica}, LANGUAGE = {eng}, ISBN = {978-1-4799-8448-0}, DOI = {10.1109/SYNASC.2014.13}, PUBLISHER = {IEEE Computer Society}, YEAR = {2014}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {SYNASC 2014}, PAGES = {34--41}, ADDRESS = {Timisoara, Romania}, }
Endnote
%0 Conference Proceedings %A Sofronie-Stokkermans, Viorica %+ Automation of Logic, MPI for Informatics, Max Planck Society %T Hierarchical Reasoning in Local Theory Extensions and Applications : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0024-C944-F %R 10.1109/SYNASC.2014.13 %D 2015 %B 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing %Z date of event: 2014-09-22 - 2014-09-25 %C Timisoara, Romania %B SYNASC 2014 %P 34 - 41 %I IEEE Computer Society %@ 978-1-4799-8448-0
Sturm, T. (2015a). Subtropical Real Root Finding. Retrieved from http://arxiv.org/abs/1501.04836
(arXiv: 1501.04836)
Abstract
We describe a new incomplete but terminating method for real root finding for large multivariate polynomials. We take an abstract view of the polynomial as the set of exponent vectors associated with sign information on the coefficients. Then we employ linear programming to heuristically find roots. There is a specialized variant for roots with exclusively positive coordinates, which is of considerable interest for applications in chemistry and systems biology. An implementation of our method combining the computer algebra system Reduce with the linear programming solver Gurobi has been successfully applied to input data originating from established mathematical models used in these areas. We have solved several hundred problems with up to more than 800000 monomials in up to 10 variables with degrees up to 12. Our method has failed due to its incompleteness in less than 8 percent of the cases.
Export
BibTeX
@online{SturmarXiv2015, TITLE = {Subtropical Real Root Finding}, AUTHOR = {Sturm, Thomas}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1501.04836}, EPRINT = {1501.04836}, EPRINTTYPE = {arXiv}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, ABSTRACT = {We describe a new incomplete but terminating method for real root finding for large multivariate polynomials. We take an abstract view of the polynomial as the set of exponent vectors associated with sign information on the coefficients. Then we employ linear programming to heuristically find roots. There is a specialized variant for roots with exclusively positive coordinates, which is of considerable interest for applications in chemistry and systems biology. An implementation of our method combining the computer algebra system Reduce with the linear programming solver Gurobi has been successfully applied to input data originating from established mathematical models used in these areas. We have solved several hundred problems with up to more than 800000 monomials in up to 10 variables with degrees up to 12. Our method has failed due to its incompleteness in less than 8 percent of the cases.}, }
Endnote
%0 Report %A Sturm, Thomas %+ Automation of Logic, MPI for Informatics, Max Planck Society %T Subtropical Real Root Finding : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0024-9D87-0 %U http://arxiv.org/abs/1501.04836 %D 2015 %X We describe a new incomplete but terminating method for real root finding for large multivariate polynomials. We take an abstract view of the polynomial as the set of exponent vectors associated with sign information on the coefficients. Then we employ linear programming to heuristically find roots. There is a specialized variant for roots with exclusively positive coordinates, which is of considerable interest for applications in chemistry and systems biology. An implementation of our method combining the computer algebra system Reduce with the linear programming solver Gurobi has been successfully applied to input data originating from established mathematical models used in these areas. We have solved several hundred problems with up to more than 800000 monomials in up to 10 variables with degrees up to 12. Our method has failed due to its incompleteness in less than 8 percent of the cases. %K Computer Science, Symbolic Computation, cs.SC
Sturm, T. (2015b). Subtropical Real Root Finding. In ISSAC’15, 40th International Symposium on Symbolic and Algebraic Computation. Bath, UK: ACM. doi:10.1145/2755996.2756677
Export
BibTeX
@inproceedings{SturmISSAC2015, TITLE = {Subtropical Real Root Finding}, AUTHOR = {Sturm, Thomas}, LANGUAGE = {eng}, ISBN = {978-1-4503-3435-8}, DOI = {10.1145/2755996.2756677}, PUBLISHER = {ACM}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {ISSAC'15, 40th International Symposium on Symbolic and Algebraic Computation}, EDITOR = {Robertz, Daniel}, PAGES = {347--354}, ADDRESS = {Bath, UK}, }
Endnote
%0 Conference Proceedings %A Sturm, Thomas %+ Automation of Logic, MPI for Informatics, Max Planck Society %T Subtropical Real Root Finding : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0026-A50F-A %R 10.1145/2755996.2756677 %D 2015 %B 40th International Symposium on Symbolic and Algebraic Computation %Z date of event: 2015-07-06 - 2015-07-09 %C Bath, UK %B ISSAC'15 %E Robertz, Daniel %P 347 - 354 %I ACM %@ 978-1-4503-3435-8
Suda, M. (2015a). Variable and Clause Elimination for LTL Satisfiability Checking. Mathematics in Computer Science, 9(3). doi:10.1007/s11786-015-0240-2
Export
BibTeX
@article{VCEforLTLmacis2015, TITLE = {Variable and Clause Elimination for {LTL} Satisfiability Checking}, AUTHOR = {Suda, Martin}, LANGUAGE = {eng}, ISSN = {1661-8270}, DOI = {10.1007/s11786-015-0240-2}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, JOURNAL = {Mathematics in Computer Science}, VOLUME = {9}, NUMBER = {3}, PAGES = {327--344}, }
Endnote
%0 Journal Article %A Suda, Martin %+ Automation of Logic, MPI for Informatics, Max Planck Society %T Variable and Clause Elimination for LTL Satisfiability Checking : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0029-4AAE-5 %R 10.1007/s11786-015-0240-2 %7 2015-09-25 %D 2015 %J Mathematics in Computer Science %V 9 %N 3 %& 327 %P 327 - 344 %I Springer %C Berlin %@ false
Suda, M. (2015b). Resolution-based Methods for Linear Temporal Reasoning. Universität des Saarlandes, Saarbrücken. Retrieved from urn:nbn:de:bsz:291-scidok-62747
Export
BibTeX
@phdthesis{SudaPhd15, TITLE = {Resolution-based Methods for Linear Temporal Reasoning}, AUTHOR = {Suda, Martin}, LANGUAGE = {eng}, URL = {urn:nbn:de:bsz:291-scidok-62747}, SCHOOL = {Universit{\"a}t des Saarlandes}, ADDRESS = {Saarbr{\"u}cken}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, }
Endnote
%0 Thesis %A Suda, Martin %Y Weidenbach, Christoph %A referee: Hoffmann, Jörg %+ 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 Resolution-based Methods for Linear Temporal Reasoning : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0028-FC90-3 %U urn:nbn:de:bsz:291-scidok-62747 %I Universität des Saarlandes %C Saarbrücken %D 2015 %P 233 p. %V phd %9 phd %U http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=dehttp://scidok.sulb.uni-saarland.de/volltexte/2015/6274/
Teucke, A., & Weidenbach, C. (2015a). First-order Logic Theorem Proving and Model Building via Approximation and Instantiation. In Frontiers of Combining Systems (FroCoS 2015). Wrocław, Poland: Springer. doi:10.1007/978-3-319-24246-0_6
Export
BibTeX
@inproceedings{TeuckeFroCoS2015, TITLE = {First-order Logic Theorem Proving and Model Building via Approximation and Instantiation}, AUTHOR = {Teucke, Andreas and Weidenbach, Christoph}, LANGUAGE = {eng}, ISBN = {978-3-319-2424}, DOI = {10.1007/978-3-319-24246-0_6}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Frontiers of Combining Systems (FroCoS 2015)}, EDITOR = {Lutz, Carsten and Ranise, Silvio}, PAGES = {85--100}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {9322}, ADDRESS = {Wroc{\l}aw, Poland}, }
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 First-order Logic Theorem Proving and Model Building via Approximation and Instantiation : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0028-8F0B-2 %R 10.1007/978-3-319-24246-0_6 %D 2015 %B 10th International Symposium on Frontiers of Combining Systems %Z date of event: 2015-09-21 - 2015-09-24 %C Wrocław, Poland %B Frontiers of Combining Systems %E Lutz, Carsten; Ranise, Silvio %P 85 - 100 %I Springer %@ 978-3-319-2424 %B Lecture Notes in Artificial Intelligence %N 9322
Teucke, A., & Weidenbach, C. (2015b). First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation. Retrieved from http://arxiv.org/abs/1503.02971
(arXiv: 1503.02971)
Abstract
Counterexample-guided abstraction refinement is a well-established technique in verification. In this paper we instantiate the idea for first-order logic theorem proving. Given a clause set $N$ we propose its abstraction into a clause set $N'$ belonging to a decidable first-order fragment. The abstraction preserves satisfiability: if $N'$ is satisfiable, so is $N$. A refutation in $N'$ can then either be lifted to a refutation in $N$, or it guides a refinement of $N$ and its abstraction $N'$ excluding the previously found refutation that is not liftable.
Export
BibTeX
@online{TeuckeWeidenbacharXiv2015, TITLE = {First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation}, AUTHOR = {Teucke, Andreas and Weidenbach, Christoph}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1503.02971}, EPRINT = {1503.02971}, EPRINTTYPE = {arXiv}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, ABSTRACT = {Counterexample-guided abstraction refinement is a well-established technique in verification. In this paper we instantiate the idea for first-order logic theorem proving. Given a clause set $N$ we propose its abstraction into a clause set $N'$ belonging to a decidable first-order fragment. The abstraction preserves satisfiability: if $N'$ is satisfiable, so is $N$. A refutation in $N'$ can then either be lifted to a refutation in $N$, or it guides a refinement of $N$ and its abstraction $N'$ excluding the previously found refutation that is not liftable.}, }
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 First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0025-694C-5 %U http://arxiv.org/abs/1503.02971 %D 2015 %8 10.03.2015 %X Counterexample-guided abstraction refinement is a well-established technique in verification. In this paper we instantiate the idea for first-order logic theorem proving. Given a clause set $N$ we propose its abstraction into a clause set $N'$ belonging to a decidable first-order fragment. The abstraction preserves satisfiability: if $N'$ is satisfiable, so is $N$. A refutation in $N'$ can then either be lifted to a refutation in $N$, or it guides a refinement of $N$ and its abstraction $N'$ excluding the previously found refutation that is not liftable. %K Computer Science, Logic in Computer Science, cs.LO
Voigt, M., & Weidenbach, C. (2015). Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete. Retrieved from http://arxiv.org/abs/1501.07209
(arXiv: 1501.07209)
Abstract
Linear arithmetic extended with free predicate symbols is undecidable, in general. We show that the restriction of linear arithmetic inequations to simple bounds extended with the Bernays-Sch\"onfinkel-Ramsey free first-order fragment is decidable and NEXPTIME-complete. The result is almost tight because the Bernays-Sch\"onfinkel-Ramsey fragment is undecidable in combination with linear difference inequations, simple additive inequations, quotient inequations and multiplicative inequations.
Export
BibTeX
@online{VoigtWeidenbacharXiv2015, TITLE = {Bernays-Sch{\"o}nfinkel-Ramsey with Simple Bounds is {NEXPTIME}-complete}, AUTHOR = {Voigt, Marco and Weidenbach, Christoph}, URL = {http://arxiv.org/abs/1501.07209}, EPRINT = {1501.07209}, EPRINTTYPE = {arXiv}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, ABSTRACT = {Linear arithmetic extended with free predicate symbols is undecidable, in general. We show that the restriction of linear arithmetic inequations to simple bounds extended with the Bernays-Sch\"onfinkel-Ramsey free first-order fragment is decidable and NEXPTIME-complete. The result is almost tight because the Bernays-Sch\"onfinkel-Ramsey fragment is undecidable in combination with linear difference inequations, simple additive inequations, quotient inequations and multiplicative inequations.}, }
Endnote
%0 Report %A Voigt, Marco %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete : %U http://hdl.handle.net/11858/00-001M-0000-0024-AA87-2 %U http://arxiv.org/abs/1501.07209 %D 2015 %X Linear arithmetic extended with free predicate symbols is undecidable, in general. We show that the restriction of linear arithmetic inequations to simple bounds extended with the Bernays-Sch\"onfinkel-Ramsey free first-order fragment is decidable and NEXPTIME-complete. The result is almost tight because the Bernays-Sch\"onfinkel-Ramsey fragment is undecidable in combination with linear difference inequations, simple additive inequations, quotient inequations and multiplicative inequations. %K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Computational Complexity, cs.CC
Weidenbach, C. (2015). Automated Reasoning Building Blocks. In Correct System Design. Oldenburg, Germany: Springer. doi:10.1007/978-3-319-23506-6_12
Export
BibTeX
@inproceedings{WeidenbachCorrectSD2015, TITLE = {Automated Reasoning Building Blocks}, AUTHOR = {Weidenbach, Christoph}, LANGUAGE = {eng}, ISBN = {978-3-319-23505-9}, DOI = {10.1007/978-3-319-23506-6_12}, PUBLISHER = {Springer}, YEAR = {2015}, MARGINALMARK = {$\bullet$}, DATE = {2015}, BOOKTITLE = {Correct System Design}, DEBUG = {author: Wehrheim, Heike}, EDITOR = {Meyer, Roland and Platzer, Andr{\'e}}, PAGES = {172--188}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {9360}, ADDRESS = {Oldenburg, Germany}, }
Endnote
%0 Conference Proceedings %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society %T Automated Reasoning Building Blocks : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0028-8EBD-7 %R 10.1007/978-3-319-23506-6_12 %D 2015 %B Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday %Z date of event: 2015-09-08 - 2015-09-09 %C Oldenburg, Germany %B Correct System Design %E Meyer, Roland; Platzer, André; Wehrheim, Heike %P 172 - 188 %I Springer %@ 978-3-319-23505-9 %B Lecture Notes in Computer Science %N 9360