Peter Baumgartner 0001
40 publications
9 venues
H Index 24
Affiliation
Data61, CSIRONICTA, Canberra Research Lab
The Australian National University
MPI Saarbr cken, Germany
University of Koblenz-Landau, Koblenz, Germany
Links
| Name | Venue | Year | citations |
|---|---|---|---|
Automated Theorem Provers Help Improve Large Language Model Reasoning.
|
LPAR | 2024 | 10 |
| Bottom-Up Stratified Probabilistic Logic Programming with Fusemate.
|
ICLP | 2023 | 3 |
| The Fusemate Logic Programming System.
|
CADE | 2021 | 5 |
| Heuristic Search Planning With Multi-Objective Probabilistic LTL Constraints.
|
KR | 2018 | 9 |
| Tableaux for Policy Synthesis for MDPs with PCTL* Constraints.
|
TABLEAUX | 2017 | 2 |
| SMTtoTPTP - A Converter for Theorem Proving Formats.
|
CADE | 2015 | 8 |
| Beagle - A Hierarchic Superposition Theorem Prover.
|
CADE | 2015 | 27 |
| Hierarchic Superposition with Weak Abstraction.
|
CADE | 2013 | 63 |
| Proving Infinite Satisfiability.
|
LPAR | 2013 | 2 |
| Tableaux for Verification of Data-Centric Processes.
|
TABLEAUX | 2013 | 2 |
| The TPTP Typed First-Order Form with Arithmetic.
|
LPAR | 2012 | 75 |
| Model Evolution with Equality Modulo Built-in Theories.
|
CADE | 2011 | 25 |
| Superposition and Model Evolution Combined.
|
CADE | 2009 | 14 |
| A Novel Architecture for Situation Awareness Systems.
|
TABLEAUX | 2009 | 58 |
| The model evolution calculus as a first-order DPLL method.
|
Artificial Intelligence | 2008 | 45 |
| (LIA) - Model Evolution with Linear Integer Arithmetic Constraints.
|
LPAR | 2008 | 32 |
| Hyper Tableaux with Equality.
|
CADE | 2007 | 57 |
| Logical Engineering with Instance-Based Methods.
|
CADE | 2007 | 15 |
| Lemma Learning in the Model Evolution Calculus.
|
LPAR | 2006 | 37 |
| The Model Evolution Calculus with Equality.
|
CADE | 2005 | 40 |
| Logic Programming Infrastructure for Inferences on FrameNet.
|
JELIA | 2004 | 9 |
| 'Living Book': -'Deduction', 'Slicing', 'Interaction'.
|
CADE | 2003 | 5 |
| The Model Evolution Calculus.
|
CADE | 2003 | 121 |
| FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure.
|
CADE | 2000 | 78 |
| Workshop: Model Computation - Principles, Algorithms, Applications.
|
CADE | 2000 | 4 |
| A Confluent Connection Calculus.
|
CADE | 1999 | 57 |
| Hyper Tableau - The Next Generation.
|
TABLEAUX | 1998 | 48 |
| Calculi for Disjunctive Logic Programming.
|
ICLP | 1997 | 34 |
| Semantically Guided Theorem Proving for Diagnosis Applications.
|
IJCAI | 1997 | 45 |
| Computing Answers with Model Elimination.
|
Artificial Intelligence | 1997 | 32 |
| Tableaux for Diagnosis Applications.
|
TABLEAUX | 1997 | 45 |
| Hyper Tableaux.
|
JELIA | 1996 | 191 |
| Constraint Model Elimination and a PTTP-Implementation.
|
TABLEAUX | 1995 | 29 |
| Model Elimination, Logic Programming and Computing Answers.
|
IJCAI | 1995 | 62 |
| Refinements of Theory Model Elimination and a Variant without Contrapositives.
|
ECAI | 1994 | 13 |
| PROTEIN: A PROver with a Theory Extension INterface.
|
CADE | 1994 | 78 |
| Model Elimination Without Contrapositives.
|
CADE | 1994 | 28 |
| An Order Theory Resolution Calculus.
|
LPAR | 1992 | 28 |
| Consolution as a Framework for Comparing Calculi.
|
TABLEAUX | 1992 | 0 |
| A Model Elimination Calculus with Built-in Theories (Extended Abstract).
|
TABLEAUX | 1992 | 0 |