Last 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

Links

[DOI]

[PuRe]

[BibTeX]

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 logic, building on existing first-order generalizations. These techniques eliminate literals, clauses, or predicate symbols from the problem, with the aim of making it more amenable to automatic proof search. We also introduce a new technique, which we call quasipure literal elimination, that strictly subsumes pure literal elimination. The new techniques are implemented in the Zipperposition theorem prover. Our evaluation shows that they sometimes help prove problems originating from the TPTP library and Isabelle formalizations.

Links

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 logic, building on existing first-order generalizations. These techniques eliminate literals, clauses, or predicate symbols from the problem, with the aim of making it more amenable to automatic proof search. We also introduce a new technique, which we call quasipure literal elimination, that strictly subsumes pure literal elimination. The new techniques are implemented in the Zipperposition theorem prover. Our evaluation shows that they sometimes help prove problems originating from the TPTP library and Isabelle formalizations. }, }

Endnote

%0 Report %A Blanchette, Jasmin Christian %A Vukmirović, 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 logic, building on existing first-order generalizations. These techniques eliminate literals, clauses, or predicate symbols from the problem, with the aim of making it more amenable to automatic proof search. We also introduce a new technique, which we call quasipure literal elimination, that strictly subsumes pure literal elimination. The new techniques are implemented in the Zipperposition theorem prover. Our evaluation shows that they sometimes help prove problems originating from the TPTP library and Isabelle formalizations. %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

Links

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

Links

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á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

Links

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 Bernays-Sch\"onfinkel fragment over simple linear real arithmetic (HBS(SLR)) can be translated into HBS clause sets over a finite set of first-order constants. The translation preserves validity and satisfiability and it is still applicable if we extend our input with positive universally or existentially quantified verification conditions (conjectures). We call this translation a Datalog hammer. The combination of its implementation in SPASS-SPL with the Datalog reasoner VLog establishes an effective way of deciding verification conditions in the Horn fragment. We verify supervisor code for two examples: a lane change assistant in a car and an electronic control unit of a supercharged combustion engine. In this paper, we improve our Datalog hammer in several ways: we generalize it to mixed real-integer arithmetic and finite first-order sorts; we extend the class of acceptable inequalities beyond variable bounds and positively grounded inequalities; and we significantly reduce the size of the hammer output by a soft typing discipline. We call the result the sorted Datalog hammer. It not only allows us to handle more complex supervisor code and to model already considered supervisor code more concisely, but it also improves our performance on real world benchmark examples. Finally, we replace the before file-based interface between SPASS-SPL and VLog by a close coupling resulting in a single executable binary.

Links

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 Bernays-Sch\"onfinkel fragment over simple linear real arithmetic (HBS(SLR)) can be translated into HBS clause sets over a finite set of first-order constants. The translation preserves validity and satisfiability and it is still applicable if we extend our input with positive universally or existentially quantified verification conditions (conjectures). We call this translation a Datalog hammer. The combination of its implementation in SPASS-SPL with the Datalog reasoner VLog establishes an effective way of deciding verification conditions in the Horn fragment. We verify supervisor code for two examples: a lane change assistant in a car and an electronic control unit of a supercharged combustion engine. In this paper, we improve our Datalog hammer in several ways: we generalize it to mixed real-integer arithmetic and finite first-order sorts; we extend the class of acceptable inequalities beyond variable bounds and positively grounded inequalities; and we significantly reduce the size of the hammer output by a soft typing discipline. We call the result the sorted Datalog hammer. It not only allows us to handle more complex supervisor code and to model already considered supervisor code more concisely, but it also improves our performance on real world benchmark examples. Finally, we replace the before file-based interface between SPASS-SPL and VLog by a close coupling resulting in a single executable binary. }, }

Endnote

%0 Report %A Bromberger, Martin %A Dragoste, Irina %A Faqeh, Rasha %A Fetzer, Christof %A González, Larry %A Krö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 Bernays-Sch\"onfinkel fragment over simple linear real arithmetic (HBS(SLR)) can be translated into HBS clause sets over a finite set of first-order constants. The translation preserves validity and satisfiability and it is still applicable if we extend our input with positive universally or existentially quantified verification conditions (conjectures). We call this translation a Datalog hammer. The combination of its implementation in SPASS-SPL with the Datalog reasoner VLog establishes an effective way of deciding verification conditions in the Horn fragment. We verify supervisor code for two examples: a lane change assistant in a car and an electronic control unit of a supercharged combustion engine. In this paper, we improve our Datalog hammer in several ways: we generalize it to mixed real-integer arithmetic and finite first-order sorts; we extend the class of acceptable inequalities beyond variable bounds and positively grounded inequalities; and we significantly reduce the size of the hammer output by a soft typing discipline. We call the result the sorted Datalog hammer. It not only allows us to handle more complex supervisor code and to model already considered supervisor code more concisely, but it also improves our performance on real world benchmark examples. Finally, we replace the before file-based interface between SPASS-SPL and VLog by a close coupling resulting in a single executable binary. %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

Links

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ález, Larry %A Krö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

Demin, A., Rahkooy, H., & Sturm, T. (2022). F5: A REDUCE Package for Signature-based Gröbner Basis Computation. In CASC 2022 - Computer Algebra in Scientific Computing. Gebze, Turkey: HAL. Retrieved from https://hal.science/hal-03781962

Links

Export

BibTeX

@inproceedings{DeminCASC22, TITLE = {F5: {A REDUCE} Package for Signature-based {G}r{\"o}bner Basis Computation}, AUTHOR = {Demin, Alexander and Rahkooy, Hamid and Sturm, Thomas}, LANGUAGE = {eng}, URL = {https://hal.science/hal-03781962}, PUBLISHER = {HAL}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, BOOKTITLE = {CASC 2022 -- Computer Algebra in Scientific Computing}, ADDRESS = {Gebze, Turkey}, }

Endnote

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

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

Links

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ć, 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, 24. doi:10.1007/s10009-022-00670-2

Links

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$}, DATE = {2022}, JOURNAL = {International Journal on Software Tools for Technology Transfer}, VOLUME = {24}, PAGES = {691--715}, }

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 24 %& 691 %P 691 - 715 %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

Links

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

Links

Export

BibTeX

@inproceedings{Haifani_IJCAR2022, TITLE = {Connection-Minimal Abduction in $\mathcal{EL}$ via Translation to {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á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

Links

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á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 it entail an observation. As such, it can be used to explain why the observation does not follow, to repair incomplete knowledge bases, and to provide possible explanations for unexpected observations. We consider TBox abduction in the lightweight description logic EL, where the observation is a concept inclusion and the background knowledge is a TBox, i.e., a set of concept inclusions. To avoid useless answers, such problems usually come with further restrictions on the solution space and/or minimality criteria that help sort the chaff from the grain. We argue that existing minimality notions are insufficient, and introduce connection minimality. This criterion follows Occam's razor by rejecting hypotheses that use concept inclusions unrelated to the problem at hand. We show how to compute a special class of connection-minimal hypotheses in a sound and complete way. Our technique is based on a translation to first-order logic, and constructs hypotheses based on prime implicates. We evaluate a prototype implementation of our approach on ontologies from the medical domain.

Links

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 it entail an observation. As such, it can be used to explain why the observation does not follow, to repair incomplete knowledge bases, and to provide possible explanations for unexpected observations. We consider TBox abduction in the lightweight description logic EL, where the observation is a concept inclusion and the background knowledge is a TBox, i.e., a set of concept inclusions. To avoid useless answers, such problems usually come with further restrictions on the solution space and/or minimality criteria that help sort the chaff from the grain. We argue that existing minimality notions are insufficient, and introduce connection minimality. This criterion follows Occam's razor by rejecting hypotheses that use concept inclusions unrelated to the problem at hand. We show how to compute a special class of connection-minimal hypotheses in a sound and complete way. Our technique is based on a translation to first-order logic, and constructs hypotheses based on prime implicates. We evaluate a prototype implementation of our approach on ontologies from the medical domain. }, }

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 it entail an observation. As such, it can be used to explain why the observation does not follow, to repair incomplete knowledge bases, and to provide possible explanations for unexpected observations. We consider TBox abduction in the lightweight description logic EL, where the observation is a concept inclusion and the background knowledge is a TBox, i.e., a set of concept inclusions. To avoid useless answers, such problems usually come with further restrictions on the solution space and/or minimality criteria that help sort the chaff from the grain. We argue that existing minimality notions are insufficient, and introduce connection minimality. This criterion follows Occam's razor by rejecting hypotheses that use concept inclusions unrelated to the problem at hand. We show how to compute a special class of connection-minimal hypotheses in a sound and complete way. Our technique is based on a translation to first-order logic, and constructs hypotheses based on prime implicates. We evaluate a prototype implementation of our approach on ontologies from the medical domain. %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

Links

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á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 only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal model assumption is used to guide inferences that are then guaranteed to be non-redundant. Redundancy is defined with respect to a dynamically changing ordering derived from the ground literal model assumption. We prove SCL(EQ) sound and complete and provide examples where our calculus improves on superposition.

Links

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 only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal model assumption is used to guide inferences that are then guaranteed to be non-redundant. Redundancy is defined with respect to a dynamically changing ordering derived from the ground literal model assumption. We prove SCL(EQ) sound and complete and provide examples where our calculus improves on superposition. }, }

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 only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal model assumption is used to guide inferences that are then guaranteed to be non-redundant. Redundancy is defined with respect to a dynamically changing ordering derived from the ground literal model assumption. We prove SCL(EQ) sound and complete and provide examples where our calculus improves on superposition. %K Computer Science, Logic in Computer Science, cs.LO

Leutgeb, L., Moser, G., & Zuleger, F. (2022). Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. In Computer Aided Verification (CAV 2022). Haifa, Israel: Springer. doi:10.1007/978-3-031-13188-2_4

Links

Export

BibTeX

@inproceedings{Leutgeb_CAV22, TITLE = {Automated Expected Amortised Cost Analysis of Probabilistic Data Structures}, AUTHOR = {Leutgeb, Lorenz and Moser, Georg and Zuleger, Florian}, LANGUAGE = {eng}, ISBN = {978-3-031-13187-5}, URL = {https://rdcu.be/c1faB}, DOI = {10.1007/978-3-031-13188-2_4}, PUBLISHER = {Springer}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, DATE = {2022}, BOOKTITLE = {Computer Aided Verification (CAV 2022)}, EDITOR = {Shoham, Sharon and Vizel, Yakir}, PAGES = {70--91}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {13372}, ADDRESS = {Haifa, Israel}, }

Endnote

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

Lüders, C., Sturm, T., & Radulescu, O. (2022a). 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 successfully applied in systems biology, especially in chemical reaction network theory. One advantage of symbolic computation is its potential for qualitative answers to biological questions. Qualitative methods analyze dynamical input systems as formal objects, in contrast to investigating only part of the state space, as is the case with numerical simulation. However, symbolic computation tools and libraries have a different set of requirements for their input data than their numerical counterparts. A common format used in mathematical modeling of biological processes is SBML. We illustrate that the use of SBML data in symbolic computation requires significant pre-processing, incorporating external biological and mathematical expertise. ODEbase provides high quality symbolic computation input data derived from established existing biomodels, covering in particular the BioModels database.

Links

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 successfully applied in systems biology, especially in chemical reaction network theory. One advantage of symbolic computation is its potential for qualitative answers to biological questions. Qualitative methods analyze dynamical input systems as formal objects, in contrast to investigating only part of the state space, as is the case with numerical simulation. However, symbolic computation tools and libraries have a different set of requirements for their input data than their numerical counterparts. A common format used in mathematical modeling of biological processes is SBML. We illustrate that the use of SBML data in symbolic computation requires significant pre-processing, incorporating external biological and mathematical expertise. ODEbase provides high quality symbolic computation input data derived from established existing biomodels, covering in particular the BioModels database. }, }

Endnote

%0 Report %A Lü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 successfully applied in systems biology, especially in chemical reaction network theory. One advantage of symbolic computation is its potential for qualitative answers to biological questions. Qualitative methods analyze dynamical input systems as formal objects, in contrast to investigating only part of the state space, as is the case with numerical simulation. However, symbolic computation tools and libraries have a different set of requirements for their input data than their numerical counterparts. A common format used in mathematical modeling of biological processes is SBML. We illustrate that the use of SBML data in symbolic computation requires significant pre-processing, incorporating external biological and mathematical expertise. ODEbase provides high quality symbolic computation input data derived from established existing biomodels, covering in particular the BioModels database. %K Quantitative Biology, Molecular Networks, q-bio.MN,Computer Science, Symbolic Computation, cs.SC

Lüders, C., Sturm, T., & Radulescu, O. (2022b). ODEbase: A Repository of ODE Systems for Systems Biology. Bioinformatics Advances, 2(2). doi:10.1093/bioadv/vbac027

Links

Export

BibTeX

@article{Lueders2022, TITLE = {{{ODE}base}: A Repository of {ODE} Systems for Systems Biology}, AUTHOR = {L{\"u}ders, Christoph and Sturm, Thomas and Radulescu, Ovidiu}, LANGUAGE = {eng}, ISSN = {2635-0041}, DOI = {10.1093/bioadv/vbac027}, PUBLISHER = {Oxford University Press}, ADDRESS = {Oxford}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, JOURNAL = {Bioinformatics Advances}, VOLUME = {2}, NUMBER = {2}, EID = {vbac027}, }

Endnote

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

Tourret, S., & Weidenbach, C. (2022). A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column. Journal of Automated Reasoning, 66. doi:10.1007/s10817-022-09617-3

Links

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$}, DATE = {2022}, JOURNAL = {Journal of Automated Reasoning}, VOLUME = {66}, PAGES = {575--584}, }

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 %V 66 %& 575 %P 575 - 584 %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, 66. doi:10.1007/s10817-021-09613-z

Links

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}, VOLUME = {66}, PAGES = {541--564}, }

Endnote

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

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

Links

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ć, 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, 66. doi:10.1007/s10817-022-09621-7

Links

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 = {Springer}, ADDRESS = {New York, NY}, YEAR = {2022}, MARGINALMARK = {$\bullet$}, DATE = {2022}, JOURNAL = {Journal of Automated Reasoning}, VOLUME = {66}, PAGES = {499--539}, }

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 %V 66 %& 499 %P 499 - 539 %I Springer %C New York, NY %@ false