Termination Tools in Automated Reasoning

Although the foundations of computers rely on the logical principles, logical reasoning, i.e., the ability to draw conclusions from certain facts, is something they have yet to be taught. The research area of automated reasoning deals with the development of respective software systems, which is also the topic of this PhD project.

Members

Sarah Winkler

ÖAW project number

Contact

Publications

Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence
Sarah Winkler, Harald Zankl, and Aart Middeldorp
Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 335 – 351, 2013.

Termination Tools in Automated Reasoning
Sarah Winkler
PhD thesis, University of Innsbruck, 2013.

Multi-Completion with Termination Tools
Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara
Journal of Automated Reasoning 50(3), pp. 317 – 354, 2013.

AC Completion with Termination Tools
Sarah Winkler and Aart Middeldorp
Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011), Lecture Notes in Artificial Intelligence 6803, pp. 492 – 498, 2011.

Termination Tools in Ordered Completion
Sarah Winkler and Aart Middeldorp
Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Lecture Notes in Artificial Intelligence 6173, pp. 518 – 532, 2010.

Optimizing mkbTT (System Description)
Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 373 – 384, 2010.