# | | Year | Author(s) [non member] | | Title | Type | |
1 |
| Avenhaus, Jürgen |
| |
| | 2003 | [Avenhaus, Jürgen]
Hillenbrand, Thomas
[Löchner, Bernd] | | On Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233 | Journal Article | |
4 |
| Ayari, Abdelwaheb |
| |
| | 2001 | [Ayari, Abdelwaheb]
Basin, David A. | | A Higher-order Interpretation of Deductive Tableau
In: Journal of Symbolic Computation [31], 487-520 | Journal Article | |
| | 1996 | Ayari, Abdelwaheb
Basin, David A. | | Generic System Support for Deductive Program Development
In: Second International Workshop, TACAS'96: Tools and Algorithms for the Construction and Analysis of Systems, 313-328 | Proceedings Article | |
| | 1995 | Ayari, Abdelwaheb | | A Reinterpretation of the Deductive Tableaux System in Higher-Order Logic
Universität des Saarlandes | Thesis - Masters thesis | |
| | 1995 | Ayari, Abdelwaheb
Basin, David A. | | Interpretation of the Deductive Tableau in HOL
In: Proceedings of the First Isabelle Users Workshop, 91-100 | Proceedings Article | |
1 |
| |
| | 1995 | Baader, Franz
Ohlbach, Hans Jürgen | | A Multi-Dimensional Terminological Knowledge Representation Language
In: Journal of Applied Non-Classical Logics [5], 153-198 | Journal Article | |
9 |
| |
| | 2003 | Schmidt, Renate A.
[Hustadt, Ullrich] | | A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 412-426 | Proceedings Article | |
| | 2003 | Korovin, Konstantin
[Voronkov, Andrei] | | AC-compatible Knuth-Bendix Order
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 47-59 | Proceedings Article | |
| | 2003 | Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe | | Superposition modulo a Shostak Theory
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 182-196 | Proceedings Article | |
| | 2003 | Ganzinger, Harald
[Stuber, Jürgen] | | Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 335-349 | Proceedings Article | |
| | 2003 | [Gaillourdet, Jean-Marie]
Hillenbrand, Thomas
[Löchner, Bernd]
[Spies, Hendrik] | | The New WALDMEISTER Loop at Work
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 317-321 | Proceedings Article | |
| | 2003 | de Nivelle, Hans | | 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 | Proceedings Article | |
| | 1996 | Basin, David A.
Matthews, Seán
Viganò, Luca | | A Topography of Labelled Modal Logics
In: Frontiers of Combining Systems (First International Workshop, Munich, March 1996), 75-92 | Part of a Book | |
| | 1994 | Fehrer, Detlef
Hustadt, Ullrich
Jaeger, Manfred
Nonnengart, Andreas
Ohlbach, Hans Jürgen
Schmidt, Renate A.
Weidenbach, Christoph
Weydert, Emil | | Description Logics for Natural Language Processing
In: International Workshop on Description Logics '94, 80-84 | Proceedings Article | |
| | 1994 | Hustadt, Ullrich | | Do we need the closed-world assumption in knowledge representation?
In: Working Notes of the KI'94 Workshop: Reasoning about Structured Objects: Knowledge Representation meets Databases (KRDB'94), 24-26 | Proceedings Article | |
1 |
| |
| | 1994 | Bockmayr, Alexander | | Using Strong Cutting Planes in Constraint Logic Programming (Extended Abstract)
In: Operations Research '93, 18th Symposium on Operations Research, 47-49 | Proceedings Article | |
20 |
| |
| | 2001 | Bachmair, Leo
Ganzinger, Harald | | Resolution Theorem Proving
In: Handbook of Automated Reasoning, 19-99 | Part of a Book | |
| | 1998 | Bachmair, Leo
Ganzinger, Harald
Voronkov, Andrei | | Elimination of Equality via Transformation with Ordering Constraints
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 175-190 | Proceedings Article | |
| | 1998 | Bachmair, Leo
Ganzinger, Harald | | Equational Reasoning in Saturation-Based Theorem Proving
In: Automated Deduction: A Basis for Applications, 353-397 | Part of a Book | |
| | 1998 | [Bachmair, Leo]
Ganzinger, Harald | | Ordered Chaining Calculi for First-Order Theories of Transitive Relations
In: Journal of the ACM [45], 1007-1049 | Journal Article | |
| | 1998 | Bachmair, Leo
Ganzinger, Harald | | Strict Basic Superposition
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 160-174 | Proceedings Article | |
| | 1995 | Bachmair, Leo
Ganzinger, Harald | | Associative-Commutative Superposition
In: Proceedings of the 4th International Workshop on Conditional and Typed Rewrite Systems (CTRS-94), 1-14 | Proceedings Article | |
| | 1995 | Bachmair, Leo
Ganzinger, Harald
[Lynch, Christopher]
[Snyder, Wayne] | | Basic Paramodulation
In: Information and Computation [121], 172-192 | Journal Article | |
| | 1995 | Bachmair, Leo
Ganzinger, Harald
Stuber, Jürgen | | Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings
In: Recent Trends in Data Type Specification. 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, 1-29 | Proceedings Article | |