| Publication | Date of Publication | Type |
|---|
| Synthesis benchmarks for automated reasoning | 2026-02-19 | Paper |
| Merging relational database technology with constraint technology | 2024-07-11 | Paper |
| Simultaneous rigid E-unification is undecidable | 2024-06-21 | Paper |
| Program Synthesis in Saturation | 2024-04-26 | Paper |
| ALASCA: reasoning in quantified linear arithmetic | 2023-12-13 | Paper |
Getting saturated with induction
Lecture Notes in Computer Science | 2023-08-10 | Paper |
Testing a saturation-based theorem prover: experiences and challenges
Tests and Proofs | 2022-07-01 | Paper |
Testing a saturation-based theorem prover: experiences and challenges
Tests and Proofs | 2022-07-01 | Paper |
| Inductive benchmarks for automated reasoning | 2022-04-22 | Paper |
| Integer induction in saturation | 2021-12-01 | Paper |
| Making theory reasoning simpler | 2021-10-18 | Paper |
Induction with generalization in superposition reasoning
Lecture Notes in Computer Science | 2021-01-20 | Paper |
| Induction in saturation-based proof search | 2020-03-10 | Paper |
What you always wanted to know about rigid \(E\)-unification
Logics in Artificial Intelligence | 2019-10-08 | Paper |
| Unification with abstraction and theory instantiation in saturation-based reasoning | 2019-09-16 | Paper |
Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
Automated Deduction — Cade-13 | 2019-01-15 | Paper |
Proof-search in intuitionistic logic based on constraint satisfaction
Theorem Proving with Analytic Tableaux and Related Methods | 2019-01-10 | Paper |
First-order interpolation and interpolating proof systems
EPiC Series in Computing | 2019-01-10 | Paper |
| A FOOLish encoding of the next state relations of imperative programs | 2018-10-18 | Paper |
Monadic simultaneous rigid \(E\)-unification and related problems
Automata, Languages and Programming | 2018-07-04 | Paper |
Coming to terms with quantified reasoning
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | 2017-10-20 | Paper |
Knuth--bendix constraint solving is NP-complete
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Selecting the selection
Automated Reasoning | 2016-09-05 | Paper |
Finding Finite Models in Multi-sorted First-Order Logic
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Extensional crisis and proving identity
Automated Technology for Verification and Analysis | 2015-12-17 | Paper |
GoRRiLA and Hard Reality
Perspectives of Systems Informatics | 2015-12-07 | Paper |
Implementing conflict resolution
Perspectives of Systems Informatics | 2015-12-07 | Paper |
Playing with AVATAR
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Cooperating proof attempts
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
A First Class Boolean Sort in First-Order Theorem Proving and TPTP
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Playing in the grey area of proofs
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
AVATAR: The Architecture for First-Order Theorem Provers
Computer Aided Verification | 2014-09-29 | Paper |
The 481 ways to split a clause and deal with propositional variables
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
Planning with effectively propositional logic
Programming Logics | 2013-04-19 | Paper |
Harald Ganzinger's legacy: contributions to logics and programming
Programming Logics | 2013-04-19 | Paper |
EPR-based bounded model checking at word level
Automated Reasoning | 2012-09-05 | Paper |
Translating regular expression matching into transducers
Journal of Applied Logic | 2012-05-23 | Paper |
| scientific article; zbMATH DE number 5993862 (Why is no real title available?) | 2012-01-01 | Paper |
Sine qua non for large theory reasoning
Lecture Notes in Computer Science | 2011-07-29 | Paper |
On transfinite Knuth-Bendix orders
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Solving systems of linear inequalities by bound propagation
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Interpolation and symbol elimination in Vampire
Automated Reasoning | 2010-09-14 | Paper |
Evaluation of automated theorem proving on the Mizar mathematical library
Mathematical Software – ICMS 2010 | 2010-09-14 | Paper |
An AC-compatible Knuth-Bendix order.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Invariant and type inference for matrices
Lecture Notes in Computer Science | 2010-01-14 | Paper |
A logical reconstruction of reachability
Lecture Notes in Computer Science | 2010-01-05 | Paper |
How to optimize proof-search in modal logics
ACM Transactions on Computational Logic | 2009-10-21 | Paper |
A decision procedure for term algebras with queues
ACM Transactions on Computational Logic | 2009-10-21 | Paper |
Conflict Resolution
Principles and Practice of Constraint Programming - CP 2009 | 2009-10-09 | Paper |
Inter-program Properties
Static Analysis | 2009-08-18 | Paper |
Interpolation and Symbol Elimination
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
Path Feasibility Analysis for String-Manipulating Programs
Tools and Algorithms for the Construction and Analysis of Systems | 2009-03-31 | Paper |
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Integrating Linear Arithmetic into Superposition Calculus
Computer Science Logic | 2009-03-05 | Paper |
Proof Systems for Effectively Propositional Logic
Automated Reasoning | 2008-11-27 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2007-06-21 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2007-06-21 | Paper |
Foundations of Information and Knowledge Systems
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Static Analysis
Lecture Notes in Computer Science | 2006-10-31 | Paper |
Mathematical Foundations of Computer Science 2005
Lecture Notes in Computer Science | 2006-10-20 | Paper |
Mathematical Foundations of Computer Science 2005
Lecture Notes in Computer Science | 2006-10-20 | Paper |
Mechanizing Mathematical Reasoning
Lecture Notes in Computer Science | 2006-01-10 | Paper |
Efficient instance retrieval with standard and relational path indexing
Information and Computation | 2005-08-05 | Paper |
| scientific article; zbMATH DE number 2084332 (Why is no real title available?) | 2004-08-06 | Paper |
| scientific article; zbMATH DE number 2038749 (Why is no real title available?) | 2004-02-08 | Paper |
Limited resource strategy in resolution theorem proving
Journal of Symbolic Computation | 2003-08-25 | Paper |
Stratified resolution
Journal of Symbolic Computation | 2003-08-25 | Paper |
Orienting rewrite rules with the Knuth-Bendix order.
Information and Computation | 2003-08-19 | Paper |
| scientific article; zbMATH DE number 1954387 (Why is no real title available?) | 2003-07-28 | Paper |
Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
Journal of Automated Reasoning | 2003-06-09 | Paper |
| scientific article; zbMATH DE number 1905119 (Why is no real title available?) | 2003-05-21 | Paper |
| scientific article; zbMATH DE number 1759379 (Why is no real title available?) | 2002-11-25 | Paper |
| scientific article; zbMATH DE number 1809861 (Why is no real title available?) | 2002-09-30 | Paper |
Term-modal logics
Studia Logica | 2002-09-16 | Paper |
| The inverse method | 2002-08-27 | Paper |
| Equality reasoning in sequent-based calculi | 2002-07-25 | Paper |
| scientific article; zbMATH DE number 1765674 (Why is no real title available?) | 2002-07-10 | Paper |
| scientific article; zbMATH DE number 1765659 (Why is no real title available?) | 2002-07-10 | Paper |
| scientific article; zbMATH DE number 1765682 (Why is no real title available?) | 2002-07-10 | Paper |
| scientific article; zbMATH DE number 1754649 (Why is no real title available?) | 2002-06-12 | Paper |
| scientific article; zbMATH DE number 1722704 (Why is no real title available?) | 2002-03-21 | Paper |
| Term indexing | 2001-10-21 | Paper |
| scientific article; zbMATH DE number 1614708 (Why is no real title available?) | 2001-07-05 | Paper |
| scientific article; zbMATH DE number 1612553 (Why is no real title available?) | 2001-07-01 | Paper |
| scientific article; zbMATH DE number 1860670 (Why is no real title available?) | 2001-01-01 | Paper |
The ground-negative fragment of first-order logic is -complete
Journal of Symbolic Logic | 2000-07-31 | Paper |
| scientific article; zbMATH DE number 1392291 (Why is no real title available?) | 2000-01-24 | Paper |
Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem
Theoretical Computer Science | 2000-01-12 | Paper |
Monadic simultaneous rigid \(E\)-unification
Theoretical Computer Science | 2000-01-12 | Paper |
| scientific article; zbMATH DE number 1348471 (Why is no real title available?) | 1999-10-10 | Paper |
Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
Journal of Automated Reasoning | 1999-09-29 | Paper |
| scientific article; zbMATH DE number 1337623 (Why is no real title available?) | 1999-09-21 | Paper |
| scientific article; zbMATH DE number 1303344 (Why is no real title available?) | 1999-09-15 | Paper |
| scientific article; zbMATH DE number 1330135 (Why is no real title available?) | 1999-09-01 | Paper |
What you always wanted to know about rigid \(E\)-unification
Journal of Automated Reasoning | 1998-08-30 | Paper |
| scientific article; zbMATH DE number 1189065 (Why is no real title available?) | 1998-08-13 | Paper |
A note on semantics of logic programs with equality based on complete sets of E-unifiers
The Journal of Logic Programming | 1997-11-10 | Paper |
| scientific article; zbMATH DE number 1004365 (Why is no real title available?) | 1997-04-27 | Paper |
The undecidability of simultaneous rigid E-unification
Theoretical Computer Science | 1997-02-27 | Paper |
On computability by logic programs
Annals of Mathematics and Artificial Intelligence | 1996-10-20 | Paper |
The anatomy of vampire. Implementing bottom-up procedures with code trees
Journal of Automated Reasoning | 1995-12-20 | Paper |
| scientific article; zbMATH DE number 517086 (Why is no real title available?) | 1994-08-21 | Paper |
