| Publication | Date of Publication | Type |
|---|
| Automated deduction | 2024-09-11 | Paper |
| Decision procedures using model building techniques | 2024-06-21 | Paper |
A method for building models automatically. Experiments with an extension of OTTER
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
Decidability and undecidability results for propositional schemata
Journal of Artificial Intelligence Research | 2011-05-04 | Paper |
| Logic for informatics and artificial intelligence | 2011-01-27 | 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 |
\(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 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 |
Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview
International Journal of Intelligent Systems | 2008-11-07 | Paper |
Automated model building
Applied Logic Series | 2005-08-11 | Paper |
| scientific article; zbMATH DE number 1748573 (Why is no real title available?) | 2002-11-04 | Paper |
| scientific article; zbMATH DE number 1745042 (Why is no real title available?) | 2002-05-23 | Paper |
Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
Journal of Symbolic Computation | 2001-03-19 | Paper |
| scientific article; zbMATH DE number 1348455 (Why is no real title available?) | 1999-10-07 | Paper |
| scientific article; zbMATH DE number 1303444 (Why is no real title available?) | 1999-06-17 | Paper |
A new technique for verifying and correcting logic programs
Journal of Automated Reasoning | 1997-11-18 | Paper |
A generic graphic framework for combining inference tools and editing proofs and formulae
Journal of Symbolic Computation | 1996-04-11 | Paper |
| scientific article; zbMATH DE number 549974 (Why is no real title available?) | 1994-10-17 | Paper |
| scientific article; zbMATH DE number 500942 (Why is no real title available?) | 1994-03-10 | Paper |
A framework for the transfer of proofs, lemmas and strategies from classical to non classical logics
Studia Logica | 1994-01-04 | Paper |
A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
Journal Of Logic And Computation | 1993-12-06 | Paper |
A method for simultaneous search for refutations and models by equational constraint solving
Journal of Symbolic Computation | 1993-01-16 | Paper |
| scientific article; zbMATH DE number 3755908 (Why is no real title available?) | 1982-01-01 | Paper |
