| Publication | Date of Publication | Type |
|---|
Generating tokenizers with flat automata
| 2024-02-08 | Paper |
A Recursive Inclusion Checker for Recursively Defined Subtypes
Modeling and Analysis of Information Systems | 2023-01-24 | Paper |
An algorithm for the retrieval of unifiers from discrimination trees
Logics in Artificial Intelligence | 2019-10-08 | Paper |
A classification of non-liftable orders for resolution
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
Subsumption algorithms for three-valued geometric resolution
Logical Methods in Computer Science | 2019-01-18 | Paper |
Theorem proving for classical logic with partial functions by reduction to Kleene logic
Journal Of Logic And Computation | 2017-05-17 | Paper |
Subsumption algorithms for three-valued geometric resolution
Lecture Notes in Computer Science | 2016-09-05 | Paper |
scientific article; zbMATH DE number 6389558 (Why is no real title available?)
| 2015-01-22 | Paper |
Classical logic with partial functions
Journal of Automated Reasoning | 2012-07-31 | Paper |
Splitting through new proposition symbols
Logic for Programming, Artificial Intelligence, and Reasoning | 2011-05-06 | Paper |
Classical logic with partial functions
Automated Reasoning | 2010-09-14 | Paper |
Translation of resolution proofs into short first-order proofs without choice axioms.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Computing finite models by reduction to function-free clause logic
Journal of Applied Logic | 2009-03-25 | Paper |
Geometric Resolution: A Proof Procedure Based on Finite Model Search
Automated Reasoning | 2009-03-12 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Deciding regular grammar logics with converse through first-order logic
Journal of Logic, Language and Information | 2005-10-04 | Paper |
Translation of resolution proofs into short first-order proofs without choice axioms
Information and Computation | 2005-08-05 | Paper |
scientific article; zbMATH DE number 2079034 (Why is no real title available?)
| 2004-07-21 | Paper |
scientific article; zbMATH DE number 1948188 (Why is no real title available?)
| 2003-07-10 | Paper |
Automated proof construction in type theory using resolution
Journal of Automated Reasoning | 2003-04-27 | Paper |
Deciding the guarded fragments by resolution
Journal of Symbolic Computation | 2003-04-02 | Paper |
Resolution in modal, description and hybrid logic
Journal of Logic and Computation | 2002-07-28 | Paper |
scientific article; zbMATH DE number 1765671 (Why is no real title available?)
| 2002-07-10 | Paper |
scientific article; zbMATH DE number 1761419 (Why is no real title available?)
| 2002-06-30 | Paper |
scientific article; zbMATH DE number 1761414 (Why is no real title available?)
| 2002-06-30 | Paper |
Deciding the \(E^+\)-class by an a posteriori, liftable order
Annals of Pure and Applied Logic | 2001-07-26 | Paper |
scientific article; zbMATH DE number 1614692 (Why is no real title available?)
| 2001-07-05 | Paper |
An overview of resolution decision procedures
| 2001-03-12 | Paper |
Resolution-based methods for modal logics
Logic Journal of the IGPL | 2000-11-07 | Paper |
scientific article; zbMATH DE number 1341615 (Why is no real title available?)
| 2000-02-17 | Paper |
scientific article; zbMATH DE number 1303345 (Why is no real title available?)
| 1999-06-17 | Paper |
An algorithm for the retrieval of unifiers from discrimination trees
Journal of Automated Reasoning | 1998-03-25 | Paper |
scientific article; zbMATH DE number 910745 (Why is no real title available?)
| 1997-04-07 | Paper |
scientific article; zbMATH DE number 517002 (Why is no real title available?)
| 1994-04-17 | Paper |
