| # | | Author/Editor | Year | | Title |
|---|
|  [1] | J. Avenhaus, T. Hillenbrand and B. Löchner | 2003 |  | On Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233 |
| [2] | P. Baumgartner and A. Burchardt | 2004 | | Logic Programming Infrastructure for Inferences on FrameNet
In: Logics in artificial intelligence : 9th European Conference, JELIA 2004, 591-603 |
| [3] | P. Baumgartner, A. Fuchs and C. Tinelli | 2004 | | Darwin: A Theorem Prover for the Model Evolution Calculus
In: Proceedings of the 1st Workshop on Empirically Successful First Order Reasoning (ESFOR'04), 1-24 |
| [4] | H. de Nivelle | 2003 | | Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 365-379 |
| [5] | H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras and C. Tinelli | 2004 | | DPLL(T): Fast Decision Procedures
In: Computer aided verification : 16th International Conference, CAV 2004, 175-188 |
| [6] | H. Ganzinger, T. Hillenbrand and U. Waldmann | 2003 | | Superposition modulo a Shostak Theory
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 182-196 |
| [7] | H. Ganzinger and K. Korovin | 2004 | | Integration of equational reasoning into instantiation-based theorem proving
In: Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL, 71-84 |
| [8] | H. Ganzinger and K. Korovin | 2003 | | New Directions in Instantiation-Based Theorem Proving
In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), 55-64 |
| [9] | H. Ganzinger, R. Nieuwenhuis and P. Nivela | 2004 | | Fast Term Indexing with Coded Context Trees
In: Journal of Automated Reasoning [32], 103-120 |
| [10] | H. Ganzinger, V. Sofronie-Stokkermans and U. Waldmann | 2004 | | Modular Proof Systems for Partial Functions with Weak Equality
In: Automated reasoning : Second International Joint Conference, IJCAR 2004, 168-182 |
| [11] | H. Ganzinger and J. Stuber | 2003 | | Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 335-349 |
| [12] | T. Hillenbrand | 2003 | | Citius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER
In: Proceedings of the 4th International Workshop on First Order Theorem Proving, FTP'03, 1-13 |
| [13] | J. Hoffmann, J. Porteous and L. Sebastia | 2004 | | Ordered Landmarks in Planning
In: Journal of Artificial Intelligence Research [22], 215-278 |
| [14] | Y. Kazakov | 2004 | | A Polynomial Translation from the Two-Variable Guarded Fragment with Number Restrictions to the Guarded Fragment
In: Logics in artificial intelligence : 9th European Conference, JELIA 2004, 372-384 |
| [15] | Y. Kazakov and H. de Nivelle | 2004 | | A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards
In: Automated reasoning : Second International Joint Conference, IJCAR 2004, 122-136 |
| [16] | K. Korovin and A. Voronkov | 2003 | | AC-compatible Knuth-Bendix Order
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 47-59 |
| [17] | P. Maier | 2004 | | Intuitionistic LTL and a New Characterization of Safety and Liveness
In: Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL, 295-309 |
| [18] | P. Maier | 2003 | | Compositional Circular Assume-Guarantee Rules Cannot Be Sound and Complete
In: Foundations of software science and computation structures : 6th International Conference, FOSSACS 2003, 343-357 |
| [19] | A. Podelski | 2004 | | Introduction to the Special Issue on Verification and Computational Logic
In: Theory and Practice of Logic Programming (TPLP) [4], 541-751 |
| [20] | A. Podelski | 2003 | | Software Model Checking with Abstraction Refinement
In: Verification, model checking, and abstract interpretation : 4th International Conference, VMCAI 2003, 1-13 |
| [21] | A. Podelski and A. Rybalchenko | 2004 | | A Complete Method for the Synthesis of Linear Ranking Functions
In: Verification, model checking, and abstract interpretation : 5th International Conference, VMCAI 2004, 239-251 |
| [22] | A. Podelski and A. Rybalchenko | 2004 | | Transition Invariants
In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, LICS 2004, 32-41 |
| [23] | S. Ratschan | 2004 | | Convergent Approximate Solving of First-order Constraints by Approximate Quantifiers
In: ACM Transactions on Computational Logic [5], 264-281 |
| [24] | S. Ratschan | 2003 | | Solving Existentially Quantified Constraints with One Equality and Arbitrarily Many Inequalities
In: Principles and practice on constraint programming - CP 2003 : 9th International Conference, CP 2003, 615-633 |
| [25] | S. Ratschan and J. Vehi | 2004 | | Robust Pole Clustering of Parametric Uncertain Systems Using Interval Methods
In: Robust control design 2003 : (ROCOND 2003) ; a proceedings volume from the 4th IFAC symposium, 323-328 |
| [26] | V. Sofronie-Stokkermans | 2004 | | Resolution-based decision procedures for the positive theory of some finitely generated varieties of algebras
In: Proceedings of the 34th International Symposium on Multiple-Valued Logic (ISMVL-2004), 32-37 |
| [27] | V. Sofronie-Stokkermans | 2003 | | Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
In: Journal of Symbolic Computation [36], 891-924 |
| 27 | | | | | |
