Automated Theorem Provers Help Improve Large Language Model Reasoning.
|
LPAR |
2024 |
0 |
Bottom-Up Stratified Probabilistic Logic Programming with Fusemate.
|
ICLP |
2023 |
0 |
The Fusemate Logic Programming System.
|
CADE |
2021 |
2 |
Heuristic Search Planning With Multi-Objective Probabilistic LTL Constraints.
|
KR |
2018 |
7 |
Tableaux for Policy Synthesis for MDPs with PCTL* Constraints.
|
TABLEAUX |
2017 |
2 |
Beagle - A Hierarchic Superposition Theorem Prover.
|
CADE |
2015 |
26 |
SMTtoTPTP - A Converter for Theorem Proving Formats.
|
CADE |
2015 |
10 |
Tableaux for Verification of Data-Centric Processes.
|
TABLEAUX |
2013 |
2 |
Proving Infinite Satisfiability.
|
LPAR |
2013 |
2 |
Hierarchic Superposition with Weak Abstraction.
|
CADE |
2013 |
60 |
The TPTP Typed First-Order Form with Arithmetic.
|
LPAR |
2012 |
62 |
Model Evolution with Equality Modulo Built-in Theories.
|
CADE |
2011 |
24 |
A Novel Architecture for Situation Awareness Systems.
|
TABLEAUX |
2009 |
59 |
Superposition and Model Evolution Combined.
|
CADE |
2009 |
14 |
(LIA) - Model Evolution with Linear Integer Arithmetic Constraints.
|
LPAR |
2008 |
33 |
The model evolution calculus as a first-order DPLL method.
|
Artificial Intelligence |
2008 |
43 |
Hyper Tableaux with Equality.
|
CADE |
2007 |
60 |
Logical Engineering with Instance-Based Methods.
|
CADE |
2007 |
15 |
Lemma Learning in the Model Evolution Calculus.
|
LPAR |
2006 |
42 |
The Model Evolution Calculus with Equality.
|
CADE |
2005 |
44 |
Logic Programming Infrastructure for Inferences on FrameNet.
|
JELIA |
2004 |
8 |
'Living Book': -'Deduction', 'Slicing', 'Interaction'.
|
CADE |
2003 |
4 |
The Model Evolution Calculus.
|
CADE |
2003 |
127 |
Workshop: Model Computation - Principles, Algorithms, Applications.
|
CADE |
2000 |
4 |
FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure.
|
CADE |
2000 |
77 |
A Confluent Connection Calculus.
|
CADE |
1999 |
57 |
Hyper Tableau - The Next Generation.
|
TABLEAUX |
1998 |
49 |
Computing Answers with Model Elimination.
|
Artificial Intelligence |
1997 |
35 |
Tableaux for Diagnosis Applications.
|
TABLEAUX |
1997 |
47 |
Calculi for Disjunctive Logic Programming.
|
ICLP |
1997 |
1 |
Semantically Guided Theorem Proving for Diagnosis Applications.
|
IJCAI |
1997 |
43 |
Hyper Tableaux.
|
JELIA |
1996 |
188 |
Model Elimination, Logic Programming and Computing Answers.
|
IJCAI |
1995 |
64 |
Constraint Model Elimination and a PTTP-Implementation.
|
TABLEAUX |
1995 |
29 |
Model Elimination Without Contrapositives.
|
CADE |
1994 |
31 |
PROTEIN: A PROver with a Theory Extension INterface.
|
CADE |
1994 |
79 |
Refinements of Theory Model Elimination and a Variant without Contrapositives.
|
ECAI |
1994 |
13 |
An Order Theory Resolution Calculus.
|
LPAR |
1992 |
27 |
Consolution as a Framework for Comparing Calculi.
|
TABLEAUX |
1992 |
0 |
A Model Elimination Calculus with Built-in Theories (Extended Abstract).
|
TABLEAUX |
1992 |
0 |