| Publication | Date of Publication | Type |
|---|
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
| 2024-04-26 | Paper |
Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
Journal of Automated Reasoning | 2023-06-14 | Paper |
Completion procedures as semidecision procedures
Conditional and Typed Rewriting Systems | 2023-03-09 | Paper |
An application of automated equational reasoning to many-valued logic
Conditional and Typed Rewriting Systems | 2023-03-09 | Paper |
Larry Wos: visions of automated reasoning
Journal of Automated Reasoning | 2022-12-12 | Paper |
Set of support, demodulation, paramodulation: a historical perspective
Journal of Automated Reasoning | 2022-12-12 | Paper |
On fairness of completion-based theorem proving strategies
Rewriting Techniques and Applications | 2022-12-09 | Paper |
SGGS decision procedures
| 2022-11-09 | Paper |
Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
Journal of Automated Reasoning | 2022-03-25 | Paper |
Theory combination: beyond equality sharing
| 2020-06-04 | Paper |
Conflict-driven satisfiability for theory combination: transition system and completeness
Journal of Automated Reasoning | 2020-03-03 | Paper |
The clause-diffusion theorem prover Peers-mcd (system description)
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
Semantically-guided goal-sensitive reasoning: inference system and completeness
Journal of Automated Reasoning | 2018-04-03 | Paper |
Satisfiability modulo theories and assignments
| 2017-09-22 | Paper |
Abstract canonical inference
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
New results on rewrite-based satisfiability procedures
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Interpolation systems for ground proofs in automated deduction: a survey
Journal of Automated Reasoning | 2016-05-26 | Paper |
Semantically-guided goal-sensitive reasoning: model representation
Journal of Automated Reasoning | 2016-05-26 | Paper |
On First-Order Model-Based Reasoning
Lecture Notes in Computer Science | 2015-09-14 | Paper |
On interpolation in automated theorem proving
Journal of Automated Reasoning | 2015-07-02 | Paper |
Rewrite-based satisfiability procedures for recursive data structures
Electronic Notes in Theoretical Computer Science | 2013-12-06 | Paper |
Rewrite-based decision procedures
Electronic Notes in Theoretical Computer Science | 2013-12-06 | Paper |
Canonical ground Horn theories
Programming Logics | 2013-04-19 | Paper |
On deciding satisfiability by theorem proving with speculative inferences
Journal of Automated Reasoning | 2012-07-31 | Paper |
On interpolation in decision procedures
Lecture Notes in Computer Science | 2011-07-01 | Paper |
Theory decision by decomposition
Journal of Symbolic Computation | 2009-12-03 | Paper |
On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
Automated Reasoning | 2009-03-12 | Paper |
${\mathcal{T}}$ -Decision by Decomposition
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Canonical Inference for Implicational Systems
Automated Reasoning | 2008-11-27 | Paper |
On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
Journal Of Logic And Computation | 2008-03-12 | Paper |
Towards a unified model of search in theorem-proving: subgoal-reduction strategies
Journal of Symbolic Computation | 2007-10-19 | Paper |
Frontiers of Combining Systems
Lecture Notes in Computer Science | 2006-10-10 | Paper |
scientific article; zbMATH DE number 1765690 (Why is no real title available?)
| 2002-07-10 | Paper |
A taxonomy of parallel strategies for deduction
Annals of Mathematics and Artificial Intelligence | 2002-06-27 | Paper |
scientific article; zbMATH DE number 1418280 (Why is no real title available?)
| 2002-04-30 | Paper |
A model and a first analysis of distributed-search contraction-based strategies
Annals of Mathematics and Artificial Intelligence | 2000-06-07 | Paper |
scientific article; zbMATH DE number 1301749 (Why is no real title available?)
| 1999-06-16 | Paper |
On the modelling of search in theorem proving -- towards a theory of strategy analysis
Information and Computation | 1999-03-22 | Paper |
scientific article; zbMATH DE number 1254024 (Why is no real title available?)
| 1999-02-23 | Paper |
PSATO: A distributed propositional prover and its application to quasigroup problems
Journal of Symbolic Computation | 1997-06-16 | Paper |
Towards a foundation of completion procedures as semidecision procedures
Theoretical Computer Science | 1997-02-28 | Paper |
On the reconstruction of proofs in distributed theorem proving: A Modified Clause-Diffusion method
Journal of Symbolic Computation | 1997-02-20 | Paper |
scientific article; zbMATH DE number 794244 (Why is no real title available?)
| 1996-05-28 | Paper |
Distributed deduction by clause-diffusion: Distributed contraction and the Aquarius prover
Journal of Symbolic Computation | 1996-04-11 | Paper |
On subsumption in distributed derivations
Journal of Automated Reasoning | 1994-11-10 | Paper |
scientific article; zbMATH DE number 512823 (Why is no real title available?)
| 1994-03-10 | Paper |
On rewrite programs: Semantics and relationship with prolog
The Journal of Logic Programming | 1992-11-10 | Paper |
