| Publication | Date of Publication | Type |
|---|
| A complete semantic back chaining proof system | 2023-04-28 | Paper |
Conditional term rewriting and first-order theorem proving
Conditional Term Rewriting Systems | 2023-03-09 | Paper |
Polynomial time termination and constraint satisfaction tests
Rewriting Techniques and Applications | 2022-12-09 | Paper |
| The aspect calculus | 2020-03-10 | Paper |
The search efficiency of theorem proving strategies
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
Semantically guided first-order theorem proving using hyper-linking
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
Semantically-guided goal-sensitive reasoning: inference system and completeness
Journal of Automated Reasoning | 2018-04-03 | Paper |
Semantically-guided goal-sensitive reasoning: model representation
Journal of Automated Reasoning | 2016-05-26 | Paper |
History and prospects for first-order automated deduction
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
The Relative Power of Semantics and Unification
Programming Logics | 2013-04-19 | Paper |
| scientific article; zbMATH DE number 5185574 (Why is no real title available?) | 2007-08-31 | Paper |
Automated Reasoning with Analytic Tableaux and Related Methods
Lecture Notes in Computer Science | 2006-07-07 | Paper |
A relevance restriction strategy for automated deduction
Artificial Intelligence | 2006-02-07 | Paper |
A satisfiability procedure for quantified Boolean formulae
Discrete Applied Mathematics | 2003-09-15 | Paper |
Ordered semantic hyper tableaux
Journal of Automated Reasoning | 2003-04-28 | Paper |
| Rewriting | 2002-08-27 | Paper |
The complexity of some complementation problems
Information Processing Letters | 2002-07-25 | Paper |
General algorithms for permutations in equational inference
Journal of Automated Reasoning | 2002-05-21 | Paper |
Ordered semantic hyper-linking
Journal of Automated Reasoning | 2001-02-06 | Paper |
| scientific article; zbMATH DE number 1507183 (Why is no real title available?) | 2000-09-14 | Paper |
Theory of partial-order programming
Science of Computer Programming | 2000-06-27 | Paper |
| scientific article; zbMATH DE number 695096 (Why is no real title available?) | 2000-06-21 | Paper |
| scientific article; zbMATH DE number 1439761 (Why is no real title available?) | 2000-05-07 | Paper |
Special cases and substitutes for rigid \(E\)-unification
Applicable Algebra in Engineering, Communication and Computing | 2000-03-05 | Paper |
| scientific article; zbMATH DE number 1113998 (Why is no real title available?) | 1998-07-13 | Paper |
Automated deduction techniques for classification in description logic systems
Journal of Automated Reasoning | 1998-04-13 | Paper |
| scientific article; zbMATH DE number 1037485 (Why is no real title available?) | 1997-07-22 | Paper |
Proof lengths for equational completion
Information and Computation | 1996-12-12 | Paper |
Problem solving by searching for models with a theorem prover
Artificial Intelligence | 1996-02-26 | Paper |
On the mechanical derivation of loop invariants
Journal of Symbolic Computation | 1995-01-12 | Paper |
Correctness of unification without occur check in prolog
The Journal of Logic Programming | 1994-04-17 | Paper |
Eliminating dublication with the hyper-linking strategy
Journal of Automated Reasoning | 1994-01-02 | Paper |
An algorithm for finding canonical sets of ground rewrite rules in polynomial time
Journal of the ACM | 1993-05-16 | Paper |
A semantic backward chaining proof system
Artificial Intelligence | 1992-09-27 | Paper |
Rewrite, rewrite, rewrite, rewrite, rewrite, \dots
Theoretical Computer Science | 1992-06-25 | Paper |
Term rewriting: Some experimental results
Journal of Symbolic Computation | 1991-01-01 | Paper |
| scientific article; zbMATH DE number 4155933 (Why is no real title available?) | 1990-01-01 | Paper |
Rigid E-unification: NP-completeness and applications to equational matings
Information and Computation | 1990-01-01 | Paper |
A sequent-style model elimination strategy and a positive refinement
Journal of Automated Reasoning | 1990-01-01 | Paper |
| scientific article; zbMATH DE number 4164185 (Why is no real title available?) | 1990-01-01 | Paper |
A Heuristic Algorithm for Small Separators in Arbitrary Graphs
SIAM Journal on Computing | 1990-01-01 | Paper |
| scientific article; zbMATH DE number 4124993 (Why is no real title available?) | 1989-01-01 | Paper |
Refinements to depth-first iterative-deepening search in automatic theorem proving
Artificial Intelligence | 1989-01-01 | Paper |
Non-Horn clause logic programming without contrapositives
Journal of Automated Reasoning | 1988-01-01 | Paper |
| scientific article; zbMATH DE number 4191131 (Why is no real title available?) | 1988-01-01 | Paper |
| scientific article; zbMATH DE number 4090846 (Why is no real title available?) | 1988-01-01 | Paper |
| scientific article; zbMATH DE number 4080962 (Why is no real title available?) | 1988-01-01 | Paper |
| scientific article; zbMATH DE number 4074536 (Why is no real title available?) | 1988-01-01 | Paper |
A heuristic triangulation algorithm
Journal of Algorithms | 1987-01-01 | Paper |
| scientific article; zbMATH DE number 4016167 (Why is no real title available?) | 1987-01-01 | Paper |
A structure-preserving clause form translation
Journal of Symbolic Computation | 1986-01-01 | Paper |
A decision procedure for combinations of propositional temporal logic and other specialized theories
Journal of Automated Reasoning | 1986-01-01 | Paper |
| scientific article; zbMATH DE number 4047064 (Why is no real title available?) | 1986-01-01 | Paper |
| scientific article; zbMATH DE number 4047177 (Why is no real title available?) | 1986-01-01 | Paper |
Termination orderings for associative-commutative rewriting systems
Journal of Symbolic Computation | 1985-01-01 | Paper |
Semantic confluence tests and completion methods
Information and Control | 1985-01-01 | Paper |
The undecidability of self-embedding for term rewriting systems
Information Processing Letters | 1985-01-01 | Paper |
Complete divisibility problems for slowly utilized oracles
Theoretical Computer Science | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3921960 (Why is no real title available?) | 1985-01-01 | Paper |
New NP-hard and NP-complete polynomial and integer divisibility problems
Theoretical Computer Science | 1984-01-01 | Paper |
Heuristic matching for graphs satisfying the triangle inequality
Journal of Algorithms | 1984-01-01 | Paper |
| scientific article; zbMATH DE number 3921952 (Why is no real title available?) | 1984-01-01 | Paper |
The occur-check problem in Prolog
New Generation Computing | 1984-01-01 | Paper |
Complete problems in the first-order predicate calculus
Journal of Computer and System Sciences | 1984-01-01 | Paper |
| scientific article; zbMATH DE number 3870636 (Why is no real title available?) | 1984-01-01 | Paper |
| scientific article; zbMATH DE number 3900184 (Why is no real title available?) | 1984-01-01 | Paper |
The Travelling Salesman Problem and Minimum Matching in the Unit Square
SIAM Journal on Computing | 1983-01-01 | Paper |
A simplified problem reduction format
Artificial Intelligence | 1982-01-01 | Paper |
Theorem proving with abstraction
Artificial Intelligence | 1981-01-01 | Paper |
An NP-complete matching problem
Discrete Applied Mathematics | 1980-01-01 | Paper |
| scientific article; zbMATH DE number 3690750 (Why is no real title available?) | 1980-01-01 | Paper |
The Application of Multivariate Polynomials to Inference Rules and Partial Tests for Unsatisfiability
SIAM Journal on Computing | 1980-01-01 | Paper |
Fast verification, testing, and generation of large primes
Theoretical Computer Science | 1979-01-01 | Paper |
Some Polynomial and Integer Divisibility Problems are $NP$-Hard
SIAM Journal on Computing | 1978-01-01 | Paper |
Sparse complex polynomials and polynomial reducibility
Journal of Computer and System Sciences | 1977-01-01 | Paper |
| scientific article; zbMATH DE number 3558923 (Why is no real title available?) | 1972-01-01 | Paper |
