RG1
Automation of Logic

Current Year

Akbarbaglu, I., Aghababa, H. P., & Rahkooy, H. (2022). On the Algebraic Structures in A(Phi) (G). Mediterranian Journal of Mathematics, 19(3). doi:10.1007/s00009-022-02052-z
Export
BibTeX
@article{Akbarbaglu22, TITLE = {On the Algebraic Structures in A(Phi) (G)}, AUTHOR = {Akbarbaglu, Ibrahim and Aghababa, Hasan P. and Rahkooy, Hamid}, LANGUAGE = {eng}, DOI = {10.1007/s00009-022-02052-z}, PUBLISHER = {Springer}, ADDRESS = {New York, NY}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, JOURNAL = {Mediterranian Journal of Mathematics}, VOLUME = {19}, NUMBER = {3}, EID = {131}, }
Endnote
%0 Journal Article %A Akbarbaglu, Ibrahim %A Aghababa, Hasan P. %A Rahkooy, Hamid %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T On the Algebraic Structures in A(Phi) (G) : %G eng %U http://hdl.handle.net/21.11116/0000-000A-A750-F %R 10.1007/s00009-022-02052-z %7 2022 %D 2022 %J Mediterranian Journal of Mathematics %V 19 %N 3 %Z sequence number: 131 %I Springer %C New York, NY
Blanchette, J. C., & Vukmirović, P. (2022). SAT-Inspired Higher-Order Eliminations. Retrieved from https://arxiv.org/abs/2208.07775
(arXiv: 2208.07775)
Abstract
We generalize several propositional preprocessing techniques to higher-order<br>logic, building on existing first-order generalizations. These techniques<br>eliminate literals, clauses, or predicate symbols from the problem, with the<br>aim of making it more amenable to automatic proof search. We also introduce a<br>new technique, which we call quasipure literal elimination, that strictly<br>subsumes pure literal elimination. The new techniques are implemented in the<br>Zipperposition theorem prover. Our evaluation shows that they sometimes help<br>prove problems originating from the TPTP library and Isabelle formalizations.<br>
Export
BibTeX
@online{Blanchette2208.07775, TITLE = {{SAT}-Inspired Higher-Order Eliminations}, AUTHOR = {Blanchette, Jasmin Christian and Vukmirovi{\'c}, Petar}, LANGUAGE = {eng}, URL = {https://arxiv.org/abs/2208.07775}, EPRINT = {2208.07775}, EPRINTTYPE = {arXiv}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, ABSTRACT = {We generalize several propositional preprocessing techniques to higher-order<br>logic, building on existing first-order generalizations. These techniques<br>eliminate literals, clauses, or predicate symbols from the problem, with the<br>aim of making it more amenable to automatic proof search. We also introduce a<br>new technique, which we call quasipure literal elimination, that strictly<br>subsumes pure literal elimination. The new techniques are implemented in the<br>Zipperposition theorem prover. Our evaluation shows that they sometimes help<br>prove problems originating from the TPTP library and Isabelle formalizations.<br>}, }
Endnote
%0 Report %A Blanchette, Jasmin Christian %A Vukmirovi&#263;, Petar %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T SAT-Inspired Higher-Order Eliminations : %G eng %U http://hdl.handle.net/21.11116/0000-000B-653C-1 %U https://arxiv.org/abs/2208.07775 %D 2022 %X We generalize several propositional preprocessing techniques to higher-order<br>logic, building on existing first-order generalizations. These techniques<br>eliminate literals, clauses, or predicate symbols from the problem, with the<br>aim of making it more amenable to automatic proof search. We also introduce a<br>new technique, which we call quasipure literal elimination, that strictly<br>subsumes pure literal elimination. The new techniques are implemented in the<br>Zipperposition theorem prover. Our evaluation shows that they sometimes help<br>prove problems originating from the TPTP library and Isabelle formalizations.<br> %K Computer Science, Logic in Computer Science, cs.LO
Bromberger, M., Gehl, T., Leutgeb, L., & Weidenbach, C. (2022). A Two-Watched Literal Scheme for First-Order Logic. In Practical Aspects of Automated Reasoning 2022 (PAAR 2022). Haifa, Israel: CEUR-WS.org. Retrieved from https://ceur-ws.org/Vol-3201/paper2.pdf; urn:nbn:de:0074-3201-6
Export
BibTeX
@inproceedings{BrombergerPAAR22, TITLE = {A Two-Watched Literal Scheme for First-Order Logic}, AUTHOR = {Bromberger, Martin and Gehl, Tobias and Leutgeb, Lorenz and Weidenbach, Christoph}, LANGUAGE = {eng}, ISSN = {1613-0073}, URL = {https://ceur-ws.org/Vol-3201/paper2.pdf; urn:nbn:de:0074-3201-6}, PUBLISHER = {CEUR-WS.org}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, BOOKTITLE = {Practical Aspects of Automated Reasoning 2022 (PAAR 2022)}, EDITOR = {Konev, Boris and Schon, Claudia and Steen, Alexander}, SERIES = {CEUR Workshop Proceedings}, VOLUME = {3201}, ADDRESS = {Haifa, Israel}, }
Endnote
%0 Conference Proceedings %A Bromberger, Martin %A Gehl, Tobias %A Leutgeb, Lorenz %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T A Two-Watched Literal Scheme for First-Order Logic : %G eng %U http://hdl.handle.net/21.11116/0000-000B-63DF-B %U https://ceur-ws.org/Vol-3201/paper2.pdf %D 2022 %B Practical Aspects of Automated Reasoning 2022 %Z date of event: 2022-08-11 - 2022-08-12 %C Haifa, Israel %B Practical Aspects of Automated Reasoning 2022 %E Konev, Boris; Schon, Claudia; Steen, Alexander %I CEUR-WS.org %B CEUR Workshop Proceedings %N 3201 %@ false
Bromberger, M., Leutgeb, L., & Weidenbach, C. (2022). An Efficient Subsumption Test Pipeline for BS(LRA) Clauses. In Automated Reasoning (IJCAR 2022). Haifa, Israel: Springer. doi:10.1007/978-3-031-10769-6_10
Export
BibTeX
@inproceedings{Bromberger_IJCAR2022, TITLE = {An Efficient Subsumption Test Pipeline for {BS(LRA)} Clauses}, AUTHOR = {Bromberger, Martin and Leutgeb, Lorenz and Weidenbach, Christoph}, LANGUAGE = {eng}, ISBN = {978-3-031-10768-9}, URL = {https://rdcu.be/cY8Pp}, DOI = {10.1007/978-3-031-10769-6_10}, PUBLISHER = {Springer}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, DATE = {2022}, BOOKTITLE = {Automated Reasoning (IJCAR 2022)}, EDITOR = {Blanchette, Jasmin Christian and Kov{\'a}cs, Laura and Pattinson, Dirk}, PAGES = {147--168}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {13385}, ADDRESS = {Haifa, Israel}, }
Endnote
%0 Conference Proceedings %A Bromberger, Martin %A Leutgeb, Lorenz %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T An Efficient Subsumption Test Pipeline for BS(LRA) Clauses : %G eng %U http://hdl.handle.net/21.11116/0000-000B-639F-3 %R 10.1007/978-3-031-10769-6_10 %U https://rdcu.be/cY8Pp %D 2022 %B 11th International Joint Conference on Automated Reasoning %Z date of event: 2022-08-08 - 2022-08-10 %C Haifa, Israel %B Automated Reasoning %E Blanchette, Jasmin Christian; Kov&#225;cs, Laura; Pattinson, Dirk %P 147 - 168 %I Springer %@ 978-3-031-10768-9 %B Lecture Notes in Artificial Intelligence %N 13385
Bromberger, M., Schwarz, S., & Weidenbach, C. (2022). Exploring Partial Models with SCL. In Practical Aspects of Automated Reasoning 2022 (PAAR 2022). Haifa, Israel: CEUR-WS.org. Retrieved from https://ceur-ws.org/Vol-3201/paper5.pdf; urn:nbn:de:0074-3201-6
Export
BibTeX
@inproceedings{BrombergerPAAR22B, TITLE = {Exploring Partial Models with {SCL}}, AUTHOR = {Bromberger, Martin and Schwarz, Simon and Weidenbach, Christoph}, LANGUAGE = {eng}, ISSN = {1613-0073}, URL = {https://ceur-ws.org/Vol-3201/paper5.pdf; urn:nbn:de:0074-3201-6}, PUBLISHER = {CEUR-WS.org}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, BOOKTITLE = {Practical Aspects of Automated Reasoning 2022 (PAAR 2022)}, EDITOR = {Konev, Boris and Schon, Claudia and Steen, Alexander}, SERIES = {CEUR Workshop Proceedings}, VOLUME = {3201}, ADDRESS = {Haifa, Israel}, }
Endnote
%0 Conference Proceedings %A Bromberger, Martin %A Schwarz, Simon %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Exploring Partial Models with SCL : %G eng %U http://hdl.handle.net/21.11116/0000-000B-63E5-3 %U https://ceur-ws.org/Vol-3201/paper5.pdf %D 2022 %B Practical Aspects of Automated Reasoning 2022 %Z date of event: 2022-08-11 - 2022-08-12 %C Haifa, Israel %B Practical Aspects of Automated Reasoning 2022 %E Konev, Boris; Schon, Claudia; Steen, Alexander %I CEUR-WS.org %B CEUR Workshop Proceedings %N 3201 %@ false
Bromberger, M., Dragoste, I., Faqeh, R., Fetzer, C., González, L., Krötzsch, M., … Weidenbach, C. (2022a). A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. Retrieved from https://arxiv.org/abs/2201.09769
(arXiv: 2201.09769)
Abstract
In a previous paper, we have shown that clause sets belonging to the Horn<br>Bernays-Sch\"onfinkel fragment over simple linear real arithmetic (HBS(SLR))<br>can be translated into HBS clause sets over a finite set of first-order<br>constants. The translation preserves validity and satisfiability and it is<br>still applicable if we extend our input with positive universally or<br>existentially quantified verification conditions (conjectures). We call this<br>translation a Datalog hammer. The combination of its implementation in<br>SPASS-SPL with the Datalog reasoner VLog establishes an effective way of<br>deciding verification conditions in the Horn fragment. We verify supervisor<br>code for two examples: a lane change assistant in a car and an electronic<br>control unit of a supercharged combustion engine. In this paper, we improve our<br>Datalog hammer in several ways: we generalize it to mixed real-integer<br>arithmetic and finite first-order sorts; we extend the class of acceptable<br>inequalities beyond variable bounds and positively grounded inequalities; and<br>we significantly reduce the size of the hammer output by a soft typing<br>discipline. We call the result the sorted Datalog hammer. It not only allows us<br>to handle more complex supervisor code and to model already considered<br>supervisor code more concisely, but it also improves our performance on real<br>world benchmark examples. Finally, we replace the before file-based interface<br>between SPASS-SPL and VLog by a close coupling resulting in a single executable<br>binary.<br>
Export
BibTeX
@online{Bromberger2201.09769, TITLE = {A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic}, AUTHOR = {Bromberger, Martin and Dragoste, Irina and Faqeh, Rasha and Fetzer, Christof and Gonz{\'a}lez, Larry and Kr{\"o}tzsch, Markus and Marx, Maximilian and Murali, Harish K. and Weidenbach, Christoph}, LANGUAGE = {eng}, URL = {https://arxiv.org/abs/2201.09769}, EPRINT = {2201.09769}, EPRINTTYPE = {arXiv}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, ABSTRACT = {In a previous paper, we have shown that clause sets belonging to the Horn<br>Bernays-Sch\"onfinkel fragment over simple linear real arithmetic (HBS(SLR))<br>can be translated into HBS clause sets over a finite set of first-order<br>constants. The translation preserves validity and satisfiability and it is<br>still applicable if we extend our input with positive universally or<br>existentially quantified verification conditions (conjectures). We call this<br>translation a Datalog hammer. The combination of its implementation in<br>SPASS-SPL with the Datalog reasoner VLog establishes an effective way of<br>deciding verification conditions in the Horn fragment. We verify supervisor<br>code for two examples: a lane change assistant in a car and an electronic<br>control unit of a supercharged combustion engine. In this paper, we improve our<br>Datalog hammer in several ways: we generalize it to mixed real-integer<br>arithmetic and finite first-order sorts; we extend the class of acceptable<br>inequalities beyond variable bounds and positively grounded inequalities; and<br>we significantly reduce the size of the hammer output by a soft typing<br>discipline. We call the result the sorted Datalog hammer. It not only allows us<br>to handle more complex supervisor code and to model already considered<br>supervisor code more concisely, but it also improves our performance on real<br>world benchmark examples. Finally, we replace the before file-based interface<br>between SPASS-SPL and VLog by a close coupling resulting in a single executable<br>binary.<br>}, }
Endnote
%0 Report %A Bromberger, Martin %A Dragoste, Irina %A Faqeh, Rasha %A Fetzer, Christof %A Gonz&#225;lez, Larry %A Kr&#246;tzsch, Markus %A Marx, Maximilian %A Murali, Harish K. %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic : %G eng %U http://hdl.handle.net/21.11116/0000-000B-652B-4 %U https://arxiv.org/abs/2201.09769 %D 2022 %X In a previous paper, we have shown that clause sets belonging to the Horn<br>Bernays-Sch\"onfinkel fragment over simple linear real arithmetic (HBS(SLR))<br>can be translated into HBS clause sets over a finite set of first-order<br>constants. The translation preserves validity and satisfiability and it is<br>still applicable if we extend our input with positive universally or<br>existentially quantified verification conditions (conjectures). We call this<br>translation a Datalog hammer. The combination of its implementation in<br>SPASS-SPL with the Datalog reasoner VLog establishes an effective way of<br>deciding verification conditions in the Horn fragment. We verify supervisor<br>code for two examples: a lane change assistant in a car and an electronic<br>control unit of a supercharged combustion engine. In this paper, we improve our<br>Datalog hammer in several ways: we generalize it to mixed real-integer<br>arithmetic and finite first-order sorts; we extend the class of acceptable<br>inequalities beyond variable bounds and positively grounded inequalities; and<br>we significantly reduce the size of the hammer output by a soft typing<br>discipline. We call the result the sorted Datalog hammer. It not only allows us<br>to handle more complex supervisor code and to model already considered<br>supervisor code more concisely, but it also improves our performance on real<br>world benchmark examples. Finally, we replace the before file-based interface<br>between SPASS-SPL and VLog by a close coupling resulting in a single executable<br>binary.<br> %K Computer Science, Logic in Computer Science, cs.LO
Bromberger, M., Dragoste, I., Faqeh, R., Fetzer, C., González, L., Krötzsch, M., … Weidenbach, C. (2022b). A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022). Munich, Germany: Springer. doi:10.1007/978-3-030-99524-9_27
Export
BibTeX
@inproceedings{Bromberger_TACAS2022, TITLE = {A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic}, AUTHOR = {Bromberger, Martin and Dragoste, Irina and Faqeh, Rasha and Fetzer, Christof and Gonz{\'a}lez, Larry and Kr{\"o}tzsch, Markus and Marx, Maximilian and Murali, Harish K. and Weidenbach, Christoph}, LANGUAGE = {eng}, ISBN = {978-3-030-99523-2}, DOI = {10.1007/978-3-030-99524-9_27}, PUBLISHER = {Springer}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, DATE = {2022}, BOOKTITLE = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022)}, EDITOR = {Fisman, Dana and Rosu, Grigore}, PAGES = {480--501}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {13243}, ADDRESS = {Munich, Germany}, }
Endnote
%0 Conference Proceedings %A Bromberger, Martin %A Dragoste, Irina %A Faqeh, Rasha %A Fetzer, Christof %A Gonz&#225;lez, Larry %A Kr&#246;tzsch, Markus %A Marx, Maximilian %A Murali, Harish K. %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic : %G eng %U http://hdl.handle.net/21.11116/0000-000B-6527-8 %R 10.1007/978-3-030-99524-9_27 %D 2022 %B 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems %Z date of event: 2022-04-02 - 2022-04-07 %C Munich, Germany %B Tools and Algorithms for the Construction and Analysis of Systems %E Fisman, Dana; Rosu, Grigore %P 480 - 501 %I Springer %@ 978-3-030-99523-2 %B Lecture Notes in Computer Science %N 13243
Desharnais, M., Vukmirović, P., Blanchette, J. C., & Wenzel, M. (2022). Seventeen Provers Under the Hammer. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Haifa, Israel: Schloss Dagstuhl. doi:10.4230/LIPIcs.ITP.2022.8
Export
BibTeX
@inproceedings{Desharnais22, TITLE = {Seventeen Provers Under the Hammer}, AUTHOR = {Desharnais, Martin and Vukmirovi{\'c}, Petar and Blanchette, Jasmin Christian and Wenzel, Makarius}, LANGUAGE = {eng}, ISBN = {978-3-95977-252-5}, URL = {urn:nbn:de:0030-drops-167178}, DOI = {10.4230/LIPIcs.ITP.2022.8}, PUBLISHER = {Schloss Dagstuhl}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, BOOKTITLE = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, EDITOR = {Andronick, June and Moura, Leonardo}, PAGES = {118--87}, EID = {8}, SERIES = {Leibniz International Proceedings in Informatics}, VOLUME = {237}, ADDRESS = {Haifa, Israel}, }
Endnote
%0 Conference Proceedings %A Desharnais, Martin %A Vukmirovi&#263;, Petar %A Blanchette, Jasmin Christian %A Wenzel, Makarius %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Seventeen Provers Under the Hammer : %G eng %U http://hdl.handle.net/21.11116/0000-000B-6539-4 %R 10.4230/LIPIcs.ITP.2022.8 %U urn:nbn:de:0030-drops-167178 %D 2022 %B 13th International Conference on Interactive Theorem Proving %Z date of event: 2022-08-07 - 2022-08-10 %C Haifa, Israel %B 13th International Conference on Interactive Theorem Proving %E Andronick, June; Moura, Leonardo %P 118 - 87 %Z sequence number: 8 %I Schloss Dagstuhl %@ 978-3-95977-252-5 %B Leibniz International Proceedings in Informatics %N 237 %U https://drops.dagstuhl.de/opus/volltexte/2022/16717https://doi.org/10.5281/zenodo.5940084
Frohn, F., & Fuhs, C. (2022). A Calculus for Modular Loop Acceleration and Non-Termination Proofs. International Journal on Software Tools for Technology Transfer, Early Access. doi:10.1007/s10009-022-00670-2
Export
BibTeX
@article{Frohn2022, TITLE = {A Calculus for Modular Loop Acceleration and Non-Termination Proofs}, AUTHOR = {Frohn, Florian and Fuhs, Carsten}, LANGUAGE = {eng}, ISSN = {1433-2779}, DOI = {10.1007/s10009-022-00670-2}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, JOURNAL = {International Journal on Software Tools for Technology Transfer}, VOLUME = {Early Access}, }
Endnote
%0 Journal Article %A Frohn, Florian %A Fuhs, Carsten %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T A Calculus for Modular Loop Acceleration and Non-Termination Proofs : %G eng %U http://hdl.handle.net/21.11116/0000-000B-58D4-3 %R 10.1007/s10009-022-00670-2 %7 2022 %D 2022 %J International Journal on Software Tools for Technology Transfer %O STTT %V Early Access %I Springer %C Berlin %@ false
Haifani, F., Koopmann, P., Tourret, S., & Weidenbach, C. (2022a). Connection-Minimal Abduction in EL via Translation to FOL (Extended Abstract). In Description Logics 2022 (DL 2022). Haifa, Israel: CEUR-WS.org. Retrieved from https://ceur-ws.org/Vol-3263/abstract-12.pdf; urn:nbn:de:0074-3263-4
Export
BibTeX
@inproceedings{HaifaniDL22, TITLE = {Connection-Minimal Abduction in {E}L via Translation to {FOL} (Extended Abstract)}, AUTHOR = {Haifani, Fajar and Koopmann, Patrick and Tourret, Sophie and Weidenbach, Christoph}, LANGUAGE = {eng}, ISSN = {1613-0073}, URL = {https://ceur-ws.org/Vol-3263/abstract-12.pdf; urn:nbn:de:0074-3263-4}, PUBLISHER = {CEUR-WS.org}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, BOOKTITLE = {Description Logics 2022 (DL 2022)}, EDITOR = {Arieli, Ofer and Homola, Martin and Jung, Jean Christoph and Mugnier, Marie-Laure}, SERIES = {CEUR Workshop Proceedings}, VOLUME = {3263}, ADDRESS = {Haifa, Israel}, }
Endnote
%0 Conference Proceedings %A Haifani, Fajar %A Koopmann, Patrick %A Tourret, Sophie %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Connection-Minimal Abduction in EL via Translation to FOL (Extended Abstract) : %G eng %U http://hdl.handle.net/21.11116/0000-000B-6558-1 %U https://ceur-ws.org/Vol-3263/abstract-12.pdf %D 2022 %B 35th International Workshop on Description Logics %Z date of event: 2022-08-07 - 2022-08-10 %C Haifa, Israel %B Description Logics 2022 %E Arieli, Ofer; Homola, Martin; Jung, Jean Christoph; Mugnier, Marie-Laure %I CEUR-WS.org %B CEUR Workshop Proceedings %N 3263 %@ false
Haifani, F., Koopmann, P., Tourret, S., & Weidenbach, C. (2022b). Connection-Minimal Abduction in EL via Translation to FOL. In Automated Reasoning (IJCAR 2022). Haifa, Israel: Springer. doi:10.1007/978-3-031-10769-6_12
Export
BibTeX
@inproceedings{Haifani_IJCAR2022, TITLE = {Connection-Minimal Abduction in&#160;$\mathcal {EL}$ via&#160;Translation to&#160;{FOL}}, AUTHOR = {Haifani, Fajar and Koopmann, Patrick and Tourret, Sophie and Weidenbach, Christoph}, LANGUAGE = {eng}, ISBN = {978-3-031-10768-9}, URL = {https://rdcu.be/cY8T3}, DOI = {10.1007/978-3-031-10769-6_12}, PUBLISHER = {Springer}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, DATE = {2022}, BOOKTITLE = {Automated Reasoning (IJCAR 2022)}, EDITOR = {Blanchette, Jasmin Christian and Kov{\'a}cs, Laura and Pattinson, Dirk}, PAGES = {188--207}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {13385}, ADDRESS = {Haifa, Israel}, }
Endnote
%0 Conference Proceedings %A Haifani, Fajar %A Koopmann, Patrick %A Tourret, Sophie %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Connection-Minimal Abduction in EL via Translation to FOL : %G eng %U http://hdl.handle.net/21.11116/0000-000B-63BE-0 %R 10.1007/978-3-031-10769-6_12 %U https://rdcu.be/cY8T3 %D 2022 %B 11th International Joint Conference on Automated Reasoning %Z date of event: 2022-08-08 - 2022-08-10 %C Haifa, Israel %B Automated Reasoning %E Blanchette, Jasmin Christian; Kov&#225;cs, Laura; Pattinson, Dirk %P 188 - 207 %I Springer %@ 978-3-031-10768-9 %B Lecture Notes in Artificial Intelligence %N 13385
Haifani, F., & Weidenbach, C. (2022). Semantic Relevance. In Automated Reasoning (IJCAR 2022). Haifa, Israel: Springer. doi:10.1007/978-3-031-10769-6_13
Export
BibTeX
@inproceedings{Haifani_IJCAR2022B, TITLE = {Semantic Relevance}, AUTHOR = {Haifani, Fajar and Weidenbach, Christoph}, LANGUAGE = {eng}, ISBN = {978-3-031-10768-9}, URL = {https://rdcu.be/cY8UF}, DOI = {10.1007/978-3-031-10769-6_13}, PUBLISHER = {Springer}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, DATE = {2022}, BOOKTITLE = {Automated Reasoning (IJCAR 2022)}, EDITOR = {Blanchette, Jasmin Christian and Kov{\'a}cs, Laura and Pattinson, Dirk}, PAGES = {208--227}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {13385}, ADDRESS = {Haifa, Israel}, }
Endnote
%0 Conference Proceedings %A Haifani, Fajar %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Semantic Relevance : %G eng %U http://hdl.handle.net/21.11116/0000-000B-63C9-3 %R 10.1007/978-3-031-10769-6_13 %U https://rdcu.be/cY8UF %D 2022 %B 11th International Joint Conference on Automated Reasoning %Z date of event: 2022-08-08 - 2022-08-10 %C Haifa, Israel %B Automated Reasoning %E Blanchette, Jasmin Christian; Kov&#225;cs, Laura; Pattinson, Dirk %P 208 - 227 %I Springer %@ 978-3-031-10768-9 %B Lecture Notes in Artificial Intelligence %N 13385
Haifani, F., Koopmann, P., Tourret, S., & Weidenbach, C. (2022c). Connection-minimal Abduction in EL via Translation to FOL -- Technical Report. Retrieved from https://arxiv.org/abs/2205.08449
(arXiv: 2205.08449)
Abstract
Abduction in description logics finds extensions of a knowledge base to make<br>it entail an observation. As such, it can be used to explain why the<br>observation does not follow, to repair incomplete knowledge bases, and to<br>provide possible explanations for unexpected observations. We consider TBox<br>abduction in the lightweight description logic EL, where the observation is a<br>concept inclusion and the background knowledge is a TBox, i.e., a set of<br>concept inclusions. To avoid useless answers, such problems usually come with<br>further restrictions on the solution space and/or minimality criteria that help<br>sort the chaff from the grain. We argue that existing minimality notions are<br>insufficient, and introduce connection minimality. This criterion follows<br>Occam's razor by rejecting hypotheses that use concept inclusions unrelated to<br>the problem at hand. We show how to compute a special class of<br>connection-minimal hypotheses in a sound and complete way. Our technique is<br>based on a translation to first-order logic, and constructs hypotheses based on<br>prime implicates. We evaluate a prototype implementation of our approach on<br>ontologies from the medical domain.<br>
Export
BibTeX
@online{Haifani2205.08449, TITLE = {Connection-minimal Abduction in {EL} via Translation to {FOL} -- Technical Report}, AUTHOR = {Haifani, Fajar and Koopmann, Patrick and Tourret, Sophie and Weidenbach, Christoph}, LANGUAGE = {eng}, URL = {https://arxiv.org/abs/2205.08449}, EPRINT = {2205.08449}, EPRINTTYPE = {arXiv}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, ABSTRACT = {Abduction in description logics finds extensions of a knowledge base to make<br>it entail an observation. As such, it can be used to explain why the<br>observation does not follow, to repair incomplete knowledge bases, and to<br>provide possible explanations for unexpected observations. We consider TBox<br>abduction in the lightweight description logic EL, where the observation is a<br>concept inclusion and the background knowledge is a TBox, i.e., a set of<br>concept inclusions. To avoid useless answers, such problems usually come with<br>further restrictions on the solution space and/or minimality criteria that help<br>sort the chaff from the grain. We argue that existing minimality notions are<br>insufficient, and introduce connection minimality. This criterion follows<br>Occam's razor by rejecting hypotheses that use concept inclusions unrelated to<br>the problem at hand. We show how to compute a special class of<br>connection-minimal hypotheses in a sound and complete way. Our technique is<br>based on a translation to first-order logic, and constructs hypotheses based on<br>prime implicates. We evaluate a prototype implementation of our approach on<br>ontologies from the medical domain.<br>}, }
Endnote
%0 Report %A Haifani, Fajar %A Koopmann, Patrick %A Tourret, Sophie %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Connection-minimal Abduction in EL via Translation to FOL -- Technical Report : %G eng %U http://hdl.handle.net/21.11116/0000-000B-6531-C %U https://arxiv.org/abs/2205.08449 %D 2022 %X Abduction in description logics finds extensions of a knowledge base to make<br>it entail an observation. As such, it can be used to explain why the<br>observation does not follow, to repair incomplete knowledge bases, and to<br>provide possible explanations for unexpected observations. We consider TBox<br>abduction in the lightweight description logic EL, where the observation is a<br>concept inclusion and the background knowledge is a TBox, i.e., a set of<br>concept inclusions. To avoid useless answers, such problems usually come with<br>further restrictions on the solution space and/or minimality criteria that help<br>sort the chaff from the grain. We argue that existing minimality notions are<br>insufficient, and introduce connection minimality. This criterion follows<br>Occam's razor by rejecting hypotheses that use concept inclusions unrelated to<br>the problem at hand. We show how to compute a special class of<br>connection-minimal hypotheses in a sound and complete way. Our technique is<br>based on a translation to first-order logic, and constructs hypotheses based on<br>prime implicates. We evaluate a prototype implementation of our approach on<br>ontologies from the medical domain.<br> %K Computer Science, Artificial Intelligence, cs.AI,Computer Science, Logic in Computer Science, cs.LO
Leidinger, H., & Weidenbach, C. (2022a). SCL(EQ): SCL for First-Order Logic with Equality. In Automated Reasoning (IJCAR 2022). Haifa, Israel: Springer. doi:10.1007/978-3-031-10769-6_14
Export
BibTeX
@inproceedings{Leidinger_IJCAR2022B, TITLE = {{SCL(EQ)}: {SCL} for First-Order Logic with Equality}, AUTHOR = {Leidinger, Hendrik and Weidenbach, Christoph}, LANGUAGE = {eng}, ISBN = {978-3-031-10768-9}, URL = {https://rdcu.be/cY8VZ}, DOI = {10.1007/978-3-031-10769-6_14}, PUBLISHER = {Springer}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, DATE = {2022}, BOOKTITLE = {Automated Reasoning (IJCAR 2022)}, EDITOR = {Blanchette, Jasmin Christian and Kov{\'a}cs, Laura and Pattinson, Dirk}, PAGES = {228--247}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {13385}, ADDRESS = {Haifa, Israel}, }
Endnote
%0 Conference Proceedings %A Leidinger, Hendrik %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T SCL(EQ): SCL for First-Order Logic with Equality : %G eng %U http://hdl.handle.net/21.11116/0000-000B-63D4-6 %R 10.1007/978-3-031-10769-6_14 %U https://rdcu.be/cY8VZ %D 2022 %B 11th International Joint Conference on Automated Reasoning %Z date of event: 2022-08-08 - 2022-08-10 %C Haifa, Israel %B Automated Reasoning %E Blanchette, Jasmin Christian; Kov&#225;cs, Laura; Pattinson, Dirk %P 228 - 247 %I Springer %@ 978-3-031-10768-9 %B Lecture Notes in Artificial Intelligence %N 13385
Leidinger, H., & Weidenbach, C. (2022b). SCL(EQ): SCL for First-Order Logic with Equality. Retrieved from https://arxiv.org/abs/2205.08297
(arXiv: 2205.08297)
Abstract
We propose a new calculus SCL(EQ) for first-order logic with equality that<br>only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven<br>Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal<br>model assumption is used to guide inferences that are then guaranteed to be<br>non-redundant. Redundancy is defined with respect to a dynamically changing<br>ordering derived from the ground literal model assumption. We prove SCL(EQ)<br>sound and complete and provide examples where our calculus improves on<br>superposition.<br>
Export
BibTeX
@online{Leidinger2205.08297, TITLE = {{SCL}({EQ}): {SCL} for First-Order Logic with Equality}, AUTHOR = {Leidinger, Hendrik and Weidenbach, Christoph}, LANGUAGE = {eng}, URL = {https://arxiv.org/abs/2205.08297}, EPRINT = {2205.08297}, EPRINTTYPE = {arXiv}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, ABSTRACT = {We propose a new calculus SCL(EQ) for first-order logic with equality that<br>only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven<br>Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal<br>model assumption is used to guide inferences that are then guaranteed to be<br>non-redundant. Redundancy is defined with respect to a dynamically changing<br>ordering derived from the ground literal model assumption. We prove SCL(EQ)<br>sound and complete and provide examples where our calculus improves on<br>superposition.<br>}, }
Endnote
%0 Report %A Leidinger, Hendrik %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T SCL(EQ): SCL for First-Order Logic with Equality : %G eng %U http://hdl.handle.net/21.11116/0000-000B-652E-1 %U https://arxiv.org/abs/2205.08297 %D 2022 %X We propose a new calculus SCL(EQ) for first-order logic with equality that<br>only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven<br>Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal<br>model assumption is used to guide inferences that are then guaranteed to be<br>non-redundant. Redundancy is defined with respect to a dynamically changing<br>ordering derived from the ground literal model assumption. We prove SCL(EQ)<br>sound and complete and provide examples where our calculus improves on<br>superposition.<br> %K Computer Science, Logic in Computer Science, cs.LO
Lüders, C., Sturm, T., & Radulescu, O. (2022). ODEbase: A Repository of ODE Systems for Systems Biology. Retrieved from https://arxiv.org/abs/2201.08980
(arXiv: 2201.08980)
Abstract
Recently, symbolic computation and computer algebra systems have been<br>successfully applied in systems biology, especially in chemical reaction<br>network theory. One advantage of symbolic computation is its potential for<br>qualitative answers to biological questions. Qualitative methods analyze<br>dynamical input systems as formal objects, in contrast to investigating only<br>part of the state space, as is the case with numerical simulation. However,<br>symbolic computation tools and libraries have a different set of requirements<br>for their input data than their numerical counterparts. A common format used in<br>mathematical modeling of biological processes is SBML. We illustrate that the<br>use of SBML data in symbolic computation requires significant pre-processing,<br>incorporating external biological and mathematical expertise. ODEbase provides<br>high quality symbolic computation input data derived from established existing<br>biomodels, covering in particular the BioModels database.<br>
Export
BibTeX
@online{Lueders2201.08980, TITLE = {{{ODE}base}: A Repository of {ODE} Systems for Systems Biology}, AUTHOR = {L{\"u}ders, Christoph and Sturm, Thomas and Radulescu, Ovidiu}, LANGUAGE = {eng}, URL = {https://arxiv.org/abs/2201.08980}, EPRINT = {2201.08980}, EPRINTTYPE = {arXiv}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, ABSTRACT = {Recently, symbolic computation and computer algebra systems have been<br>successfully applied in systems biology, especially in chemical reaction<br>network theory. One advantage of symbolic computation is its potential for<br>qualitative answers to biological questions. Qualitative methods analyze<br>dynamical input systems as formal objects, in contrast to investigating only<br>part of the state space, as is the case with numerical simulation. However,<br>symbolic computation tools and libraries have a different set of requirements<br>for their input data than their numerical counterparts. A common format used in<br>mathematical modeling of biological processes is SBML. We illustrate that the<br>use of SBML data in symbolic computation requires significant pre-processing,<br>incorporating external biological and mathematical expertise. ODEbase provides<br>high quality symbolic computation input data derived from established existing<br>biomodels, covering in particular the BioModels database.<br>}, }
Endnote
%0 Report %A L&#252;ders, Christoph %A Sturm, Thomas %A Radulescu, Ovidiu %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T ODEbase: A Repository of ODE Systems for Systems Biology : %G eng %U http://hdl.handle.net/21.11116/0000-000B-654F-C %U https://arxiv.org/abs/2201.08980 %D 2022 %X Recently, symbolic computation and computer algebra systems have been<br>successfully applied in systems biology, especially in chemical reaction<br>network theory. One advantage of symbolic computation is its potential for<br>qualitative answers to biological questions. Qualitative methods analyze<br>dynamical input systems as formal objects, in contrast to investigating only<br>part of the state space, as is the case with numerical simulation. However,<br>symbolic computation tools and libraries have a different set of requirements<br>for their input data than their numerical counterparts. A common format used in<br>mathematical modeling of biological processes is SBML. We illustrate that the<br>use of SBML data in symbolic computation requires significant pre-processing,<br>incorporating external biological and mathematical expertise. ODEbase provides<br>high quality symbolic computation input data derived from established existing<br>biomodels, covering in particular the BioModels database.<br> %K Quantitative Biology, Molecular Networks, q-bio.MN,Computer Science, Symbolic Computation, cs.SC
Tourret, S., & Weidenbach, C. (2022). A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column. Journal of Automated Reasoning. doi:10.1007/s10817-022-09617-3
Export
BibTeX
@article{Tourret2022, TITLE = {A Posthumous Contribution by {Larry Wos}: {E}xcerpts from an Unpublished Column}, AUTHOR = {Tourret, Sophie and Weidenbach, Christoph}, LANGUAGE = {eng}, ISSN = {0168-7433}, DOI = {10.1007/s10817-022-09617-3}, PUBLISHER = {Springer}, ADDRESS = {New York, NY}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, JOURNAL = {Journal of Automated Reasoning}, }
Endnote
%0 Journal Article %A Tourret, Sophie %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column : %G eng %U http://hdl.handle.net/21.11116/0000-0009-FACB-9 %R 10.1007/s10817-022-09617-3 %7 2022 %D 2022 %J Journal of Automated Reasoning %I Springer %C New York, NY %@ false
Vukmirović, P., Bentkamp, A., Blanchette, J. C., Cruanes, S., Nummelin, V., & Tourret, S. (2022). Making Higher-Order Superposition Work. Journal of Automated Reasoning. doi:10.1007/s10817-021-09613-z
Export
BibTeX
@article{Vukmirovic2022, TITLE = {Making Higher-Order Superposition Work}, AUTHOR = {Vukmirovi{\'c}, Petar and Bentkamp, Alexander and Blanchette, Jasmin Christian and Cruanes, Simon and Nummelin, Visa and Tourret, Sophie}, LANGUAGE = {eng}, ISSN = {0168-7433}, DOI = {10.1007/s10817-021-09613-z}, PUBLISHER = {Springer}, ADDRESS = {New York, NY}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, JOURNAL = {Journal of Automated Reasoning}, }
Endnote
%0 Journal Article %A Vukmirovi&#263;, Petar %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Cruanes, Simon %A Nummelin, Visa %A Tourret, Sophie %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Making Higher-Order Superposition Work : %G eng %U http://hdl.handle.net/21.11116/0000-0009-F7A1-A %R 10.1007/s10817-021-09613-z %7 2022 %D 2022 %J Journal of Automated Reasoning %I Springer %C New York, NY %@ false %U https://rdcu.be/cGXwx
Vukmirović, P., Blanchette, J. C., Cruanes, S., & Schulz, S. (2022). Extending a Brainiac Prover to Lambda-Free Higher-Order Logic. International Journal on Software Tools for Technology Transfer (STTT), 24. doi:10.1007/s10009-021-00639-7
Export
BibTeX
@article{Vukmirovic2021, TITLE = {Extending a Brainiac Prover to Lambda-Free Higher-Order Logic}, AUTHOR = {Vukmirovi{\'c}, Petar and Blanchette, Jasmin Christian and Cruanes, Simon and Schulz, Stephan}, LANGUAGE = {eng}, ISSN = {1433-2779}, DOI = {10.1007/s10009-021-00639-7}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, DATE = {2022}, JOURNAL = {International Journal on Software Tools for Technology Transfer (STTT)}, VOLUME = {24}, PAGES = {67--87}, }
Endnote
%0 Journal Article %A Vukmirovi&#263;, Petar %A Blanchette, Jasmin Christian %A Cruanes, Simon %A Schulz, Stephan %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Extending a Brainiac Prover to Lambda-Free Higher-Order Logic : %G eng %U http://hdl.handle.net/21.11116/0000-0009-2A64-8 %R 10.1007/s10009-021-00639-7 %7 2021 %D 2022 %J International Journal on Software Tools for Technology Transfer (STTT) %V 24 %& 67 %P 67 - 87 %I Springer %C Berlin %@ false
Waldmann, U., Tourret, S., Robillard, S., & Blanchette, J. C. (2022). A Comprehensive Framework for Saturation Theorem Proving. Journal of Automated Reasoning. doi:10.1007/s10817-022-09621-7
Export
BibTeX
@article{Waldmann_2022, TITLE = {A Comprehensive Framework for Saturation Theorem Proving}, AUTHOR = {Waldmann, Uwe and Tourret, Sophie and Robillard, Simon and Blanchette, Jasmin Christian}, LANGUAGE = {eng}, ISSN = {0168-7433}, DOI = {10.1007/s10817-022-09621-7}, PUBLISHER = {D. Reidel Pub. Co.}, ADDRESS = {Dordrecht, Holland}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, JOURNAL = {Journal of Automated Reasoning}, }
Endnote
%0 Journal Article %A Waldmann, Uwe %A Tourret, Sophie %A Robillard, Simon %A Blanchette, Jasmin Christian %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T A Comprehensive Framework for Saturation Theorem Proving : %G eng %U http://hdl.handle.net/21.11116/0000-000A-9D8A-A %R 10.1007/s10817-022-09621-7 %7 2022 %D 2022 %J Journal of Automated Reasoning %I D. Reidel Pub. Co. %C Dordrecht, Holland %@ false