| Publication | Date of Publication | Type |
|---|
Automated deduction
| 2024-09-11 | Paper |
Decision procedures using model building techniques
| 2024-06-21 | Paper |
Testing the satisfiability of formulas in separation logic with permissions
| 2024-05-17 | Paper |
A strict constrained superposition calculus for graphs
Lecture Notes in Computer Science | 2023-11-24 | Paper |
A proof procedure for separation logic with inductive definitions and data
Journal of Automated Reasoning | 2023-10-24 | Paper |
An undecidability result for separation logic with theory reasoning
Information Processing Letters | 2023-06-05 | Paper |
Unifying decidable entailments in separation logic with inductive definitions
| 2021-12-01 | Paper |
Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules
Information Processing Letters | 2021-10-19 | Paper |
The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
ACM Transactions on Computational Logic | 2020-09-11 | Paper |
Prenex separation logic with one selector field
| 2020-05-14 | Paper |
Ilinva: using abduction to generate loop invariants
| 2020-05-13 | Paper |
Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL
Journal of Automated Reasoning | 2020-04-07 | Paper |
Combining induction and saturation-based theorem proving
Journal of Automated Reasoning | 2020-03-03 | Paper |
The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains
| 2020-01-28 | Paper |
A method for building models automatically. Experiments with an extension of OTTER
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
Building proofs or counterexamples by analogy in a resolution framework
Logics in Artificial Intelligence | 2019-10-08 | Paper |
Partial matching for analogy discovery in proofs and counter-examples
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
Lecture Notes in Computer Science | 2019-01-15 | Paper |
A tableaux calculus for reducing proof size
| 2018-10-18 | Paper |
A generic framework for implicate generation modulo theories
| 2018-10-18 | Paper |
Superposition with datatypes and codatatypes
| 2018-10-18 | Paper |
CERES for first-order schemata
Journal Of Logic And Computation | 2018-02-13 | Paper |
Prime implicate generation in equational logic
Journal of Artificial Intelligence Research | 2018-01-12 | Paper |
The binomial pricing model in finance: a formalization in Isabelle
| 2017-09-22 | Paper |
A superposition calculus for abductive reasoning
Journal of Automated Reasoning | 2017-08-17 | Paper |
A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules
Journal Of Logic And Computation | 2017-05-17 | Paper |
Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
Journal of Automated Reasoning | 2016-10-27 | Paper |
Analogy in automated deduction: a survey
Computational Approaches to Analogical Reasoning: Current Trends | 2016-07-18 | Paper |
Reasoning on schemas of formulas: an automata-based approach
Language and Automata Theory and Applications | 2016-04-08 | Paper |
Quantifier-free equational logic and prime implicate generation
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Instantiation schemes for nested theories
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
A complete superposition calculus for primal grammars
Journal of Automated Reasoning | 2015-07-02 | Paper |
Tractable and intractable classes of propositional schemata
Journal Of Logic And Computation | 2015-02-11 | Paper |
A rewriting strategy to generate prime implicates in equational logic
Automated Reasoning | 2014-09-26 | Paper |
Schemata of formulæ in the theory of arrays
Lecture Notes in Computer Science | 2013-10-04 | Paper |
Combining superposition and induction: a practical realization
Frontiers of Combining Systems | 2013-09-20 | Paper |
A resolution calculus for first-order schemata
Fundamenta Informaticae | 2013-08-26 | Paper |
Completeness and decidability results for first-order clauses with indices
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
Electronic Notes in Theoretical Computer Science | 2013-04-19 | Paper |
Modular instantiation schemes
Information Processing Letters | 2013-04-04 | Paper |
Reasoning on schemata of formulæ
Lecture Notes in Computer Science | 2012-09-07 | Paper |
A calculus for generating ground explanations
Automated Reasoning | 2012-09-05 | Paper |
An instantiation scheme for satisfiability modulo theories
Journal of Automated Reasoning | 2012-07-31 | Paper |
Schemata of SMT-problems
Lecture Notes in Computer Science | 2011-07-01 | Paper |
Decidability and undecidability results for propositional schemata
Journal of Artificial Intelligence Research | 2011-05-04 | Paper |
Simplified handling of iterated term schemata
Annals of Mathematics and Artificial Intelligence | 2011-01-12 | Paper |
RegSTAB: A SAT Solver for Propositional Schemata
Automated Reasoning | 2010-09-14 | Paper |
A decidable class of nested iterated schemata
Automated Reasoning | 2010-09-14 | Paper |
Perfect discrimination graphs: indexing terms with integer exponents
Automated Reasoning | 2010-09-14 | Paper |
Instantiation of SMT problems modulo integers
Lecture Notes in Computer Science | 2010-08-24 | Paper |
\(I\)-terms in ordered resolution and superposition calculi: retrieving lost completeness
Lecture Notes in Computer Science | 2010-08-24 | Paper |
Complexity of the satisfiability problem for a class of propositional schemata
Language and Automata Theory and Applications | 2010-05-26 | Paper |
A more efficient tableaux procedure for simultaneous search for refutations and finite models
Lecture Notes in Computer Science | 2010-03-09 | Paper |
Bottom-up Construction of Semantic Tableaux
Journal Of Logic And Computation | 2010-02-19 | Paper |
Constructing infinite models represented by tree automata
Annals of Mathematics and Artificial Intelligence | 2009-12-11 | Paper |
A Schemata Calculus for Propositional Logic
Lecture Notes in Computer Science | 2009-12-01 | Paper |
A term-graph clausal logic: completeness and incompleteness results ★
Journal of Applied Non-Classical Logics | 2009-11-11 | Paper |
Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps
Logic, Language, Information and Computation | 2009-03-10 | Paper |
Automated Model Building: From Finite to Infinite Models
Lecture Notes in Computer Science | 2009-01-27 | Paper |
Narrowing Data-Structures with Pointers
Lecture Notes in Computer Science | 2008-11-27 | Paper |
Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview
International Journal of Intelligent Systems | 2008-11-07 | Paper |
A Needed Rewriting Strategy for Data-Structures with Pointers
Rewriting Techniques and Applications | 2008-08-28 | Paper |
Extended resolution simulates binary decision diagrams
Discrete Applied Mathematics | 2008-03-28 | Paper |
A Bottom-Up Approach to Clausal Tableaux
Lecture Notes in Computer Science | 2008-01-04 | Paper |
Non Strict Confluent Rewrite Systems for Data-Structures with Pointers
Lecture Notes in Computer Science | 2008-01-02 | Paper |
scientific article; zbMATH DE number 5173934 (Why is no real title available?)
| 2007-07-24 | Paper |
Some techniques for proving termination of the hyperresolution calculus
Journal of Automated Reasoning | 2007-01-30 | Paper |
Representing and building models for decidable subclasses of equational clausal logic
Journal of Automated Reasoning | 2007-01-29 | Paper |
Logics in Artificial Intelligence
Lecture Notes in Computer Science | 2006-10-25 | Paper |
scientific article; zbMATH DE number 5007860 (Why is no real title available?)
| 2006-02-21 | Paper |
A Resolution Calculus for Shortening Proofs
Logic Journal of the IGPL | 2005-10-18 | Paper |
Automated model building
Applied Logic Series | 2005-08-11 | Paper |
The first order theory of primal grammars is decidable
Theoretical Computer Science | 2004-10-01 | Paper |
scientific article; zbMATH DE number 1990014 (Why is no real title available?)
| 2003-10-12 | Paper |
Model building with ordered resolution: Extracting models from saturated clause sets
Journal of Symbolic Computation | 2003-08-25 | Paper |
A calculus combining resolution and enumeration for building finite models
Journal of Symbolic Computation | 2003-08-25 | Paper |
Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae
Logic Journal of the IGPL | 2003-08-24 | Paper |
Extracting models from clause sets saturated under semantic refinements of the resolution rule.
Information and Computation | 2003-08-19 | Paper |
scientific article; zbMATH DE number 1748573 (Why is no real title available?)
| 2002-11-04 | Paper |
scientific article; zbMATH DE number 1765701 (Why is no real title available?)
| 2002-07-10 | Paper |
scientific article; zbMATH DE number 1745042 (Why is no real title available?)
| 2002-05-23 | Paper |
On the decidability of the PVD class with equality
Logic Journal of the IGPL | 2002-03-12 | Paper |
Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
Journal of Symbolic Computation | 2001-03-19 | Paper |
Pruning the search space and extracting more models in tableaux
Logic Journal of the IGPL | 2000-12-06 | Paper |
scientific article; zbMATH DE number 1303444 (Why is no real title available?)
| 1999-06-17 | Paper |
A new method for automated finite model building exploiting failures and symmetries
Journal Of Logic And Computation | 1999-01-11 | Paper |
Semantic generalizations for proving and disproving conjectures by analogy
Journal of Automated Reasoning | 1998-06-02 | Paper |
A new technique for verifying and correcting logic programs
Journal of Automated Reasoning | 1997-11-18 | Paper |
scientific article; zbMATH DE number 1051240 (Why is no real title available?)
| 1997-08-24 | Paper |
Increasing model building capabilities by constraint solving on terms with integer exponents
Journal of Symbolic Computation | 1997-07-23 | Paper |
