Dr Peter Baumgartner
Biography
Research interests:
Advancement of automated deduction, in particular first-order logic theorem proving. Design of calculi (in particular the Model Evolution calculus), implementations (in particular the Darwin system) and their application for software verification and knowledge representation purposes; exploiting connections into related areas such as logic programming, description logics and nonmonotonic reasoning.
Advancement of automated deduction, in particular first-order logic theorem proving. Design of calculi (in particular the Model Evolution calculus), implementations (in particular the Darwin system) and their application for software verification and knowledge representation purposes; exploiting connections into related areas such as logic programming, description logics and nonmonotonic reasoning.
Available student projects
Topics in Automated Reasoning with Instance-Based Methods - Keywords: First-Order Logic, Automated Reasoning, Instance-Based Methods
Logical Analysis of Business Rules - Keywords: Business Rules, Automated Reasoning
Extending the first-order theorem prover SPASS with a new split rule - Keywords: Automated Theorem Proving, Resolution
Partially automating an interactively found proof - Keywords: Automated Theorem Proving
Publications
- Baumgartner, P, Thiebaux, S & Werndl Trevizan, F 2017, 'Tableaux for Policy Synthesis for MDPs with PCTL Constraints', 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2017, ed. R A. Schmidt and C Nalon, Springer International Publishing, Cham, Switzerland, pp. 175-192pp.
- Baumgartner, P, Bibel, W & Waldinger, R 2016, 'In Memory of Mark Stickel', Journal of Automated Reasoning, vol. 56, no. 2, pp. 95 - 98.
- Baumgartner, P 2015, 'SMTtoTPTP - A Converter for Theorem Proving Formats', Lecture Notes in Artificial Intelligence, vol. 9195, pp. 285-294.
- Baumgartner, P, Bax, J & Waldmann, U 2015, 'Beagle - A Hierarchic Superposition Theorem Prover', 25th International Conference on Automated Deduction CADE 2015, ed. Amy P. Felty, Aart Middeldorp, Springer International Publishing AG, Switzerland, pp. 367-377.
- Baumgartner, P, Bax, J & Waldmann, U 2014, 'Finite Quantification in Hierarchic Theorem Proving', 7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, ed. S Demri, D Kapur, C Weidenbach, Springer Verlag, Switzerland, pp. 152-167.
- Baumgartner, P 2014, 'Model Evolution-Based Theorem Proving', IEEE Intelligent Systems, vol. 29, no. 1, pp. 4-10.
- Baumgartner, P & Waldmann, U 2013, 'Hierarchic Superposition: Completeness without Compactness', Fifth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2013), ed. Marek Kosta and Thomas Sturm, Birkhaeuser, Germany, pp. 8-12.
- Baumgartner, P & Waldmann, U 2013, 'Hierarchic Superposition with Weak Abstraction', 24th International Conference on Automated Deduction CADE-24, ed. Goebel, Randy, Wahlster, Wolfgang, Tanaka, Yuzuru, Springer, USA, pp. 39-57.
- Baumgartner, P & Bax, J 2013, 'Proving Infinite Satisfiability', in Ken McMillan, Aart Middeldorp, Andrei Voronkov (ed.), Lecture Notes in Computer Science: Logic for Programming, Artificial Intelligence and Reasoning, Springer-Verlag Berlin Heidelberg, Heidelberg, pp. 86-95.
- Bauer, A, Baumgartner, P, Diller, M, Norrish, M. 2013, 'Tableaux for Verification of Data-Centric Processes', TABLEAUX 2013, ed. D. Galmiche and D. Larchey-Wendling, Springer-Verlag Berlin Heidelberg, USA, pp. 23-43.
- Sutcliffe, G, Schulz, S, Claessen, K et al 2012, 'The TPTP Typed First-Order Form with Arithmetic', International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2012), Springer, Unknown, pp. 406-419.
- Barnes, N, Baumgartner, P, Caetano, T et al 2012, 'AI@NICTA', AI Magazine, vol. 33, no. 3, pp. 115-127.
- Baumgartner, P, Pelzer, B & Tinelli, C 2012, 'Model Evolution with equality - Revised and Implemented', Journal of Symbolic Computation, vol. 47, no. 9, pp. 1011-1045.
- Barnes, N, Baumgartner, P, Caetano, T et al 2012, 'AI@NICTA', AI Magazine, vol. 33, no. 3, pp. 115-127.
- Baumgartner, P & Waldmann, U 2011, 'A Combined Superposition and Model Evolution Calculus', Journal of Automated Reasoning, vol. 47, no. 2, pp. 191-227.
- Baumgartner, P & Tinelli, C 2011, 'Model Evolution with Equality Modulo Built-in Theories', International Conference on Automated Deduction (CADE 2011), Springer, Verlin Heidelberg, pp. 85-100.
- Baumgartner, P & Thorstensen, E 2010, 'Instance Based Methods-A Brief Overview', Kuenstliche Intelligenz, vol. 24, no. 1, pp. 35-42.
- Baumgartner, P & Waldmann, U 2009, 'Superposition and Model Evolution Combined', International Conference on Automated Deduction (CADE 2009), ed. R A Schmidt, Springer, berlin, pp. 17-34.
- Baader, F, Bauer, A, Baumgartner, P et al 2009, 'A novel architecture for situation awareness systems', in Martin Giese, Arild Waaler (ed.), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009), Springer, Germany, pp. 77-92.
- Baumgartner, P, Fuchs, A, de Nivelle, H et al 2009, 'Computing finite models by reduction to function-free clause logic', Journal of Applied Logic, vol. 7, no. 1, pp. 58-74.
- Baumgartner, P & Slaney, J 2009, 'Constraint Modelling: A Challenge for First Order Automated Reasoning', International Workshop on First-Order Theorem Proving (FTP 2009), ed. Nicolas Peltier, Viorica Sofronie-Stokkermans, CEUR-WS.ORG, Oslo, Norway, pp. 4-18.
- Baumgartner, P, Furbach, U & Pelzer, B 2008, 'The hyper Tableaux calculus with equality and an application to finite model computation', Journal of Logic and Computation, vol. advance access 2008, pp. 1-33.
- Baumgartner, P, Fuchs, A & Tinelli, C 2008, 'ME(LIA) - Model evolution with linear integer arithmetic constraints', International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2008), ed. I. Cervesato, H. Veith, A. Voronkov, Springer, Berlin, Germany, pp. 258-273.
- Baumgartner, P & Tinelli, C 2008, 'The model evolution calculus as a first-order DPLL method', Artificial Intelligence, vol. 172, no. 4-5, pp. 591-632.
- Baumgartner, P 2007, 'Logical engineering with instance-based methods', International Conference on Automated Deduction (CADE 2007), ed. Frank Pfenning, Springer, New York, pp. 404-409.
- Baumgartner, P, Furbach, U & Pelzer, B 2007, 'Hyper tableaux with equality', International Conference on Automated Deduction (CADE 2007), ed. Frank Pfenning, Springer, New York, pp. 492-507.
- Baumgartner, P, Fuchs, A, de Nivelle, H et al 2006, 'Computing finite models by reduction to function-free clause logic', International Joint Conference on Automated Reasoning (IJCAR 2006), ed. W. Ahrendt, P. Baumgartner, H. de Nivelle, Conference Organising Committee, Seattle, WA USA, pp. 82-95.
- Baader, F, Baumgartner, P, Nieuwenhuis, R et al 2006, 'Deduction and applications', Dagstuhl Seminar 2005, ed. F. Baader, P. Baumgartner, R. Nieuwenhuis, A. Voronkov, Internationales Begegnungs und Forschungszentrum fuer Informatik, Germany.
- Baumgartner, P, Fuchs, A & Tinelli, C 2006, 'Lemma learning in the model evolution calculus', International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2006), ed. Miki Hermann, Andrei Voronkov, Springer, New York, pp. 572-586.
- Baumgartner, P, Fuchs, A & Tinelli, C 2006, 'Implementing the model evolution calculus', International Journal on Artificial Intelligence Tools, vol. 15, no. 10, pp. 21-52.
- Baumgartner, P & Schmidt, R 2006, 'Blocking and other enhancements for bottom-up model generation methods', International Joint Conference on Automated Reasoning (IJCAR 2006), ed. W. Ahrendt, P. Baumgartner, H. de Nivelle, Conference Organising Committee, Seattle, WA USA, pp. 125-139.
- Baumgartner, P & Suchanek, F 2006, 'Automated reasoning support for first-order ontologies', in J.J. Alferes, J. Bailey, W. May, U. Schwertel (ed.), Principles and Practice of Semantic Web Reasoning: 4th International Workshop, PPSWR 2006, Springer, Berlin, pp. 18-32.
Projects and Grants
Grants information is drawn from ARIES. To add or update Projects or Grants information please contact your College Research Office.
- Practical Automated Deduction (Secondary Investigator)
