| # |  | Year | Author(s) [non member] | Editor(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. | Margaria, Tiziana
Steffen, Bernhard | | 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. | Paulson, Lawrence C. | | 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 | de Nivelle, Hans | [Baader, Franz] | | 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 | |
| | 2003 | [Gaillourdet, Jean-Marie]
Hillenbrand, Thomas
[Löchner, Bernd]
[Spies, Hendrik] | [Baader, Franz] | | The New WALDMEISTER Loop at Work
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 317-321 | Proceedings Article | |
| | 2003 | Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe | [Baader, Franz] | | 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] | Baader, Franz | | 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 | Korovin, Konstantin
[Voronkov, Andrei] | [Baader, Franz] | | AC-compatible Knuth-Bendix Order
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 47-59 | Proceedings Article | |
| | 2003 | Schmidt, Renate A.
[Hustadt, Ullrich] | [Baader, Franz] | | 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 | |
| | 1996 | Basin, David A.
Matthews, Seán
Viganò, Luca | Baader, Franz
Schulz, Klaus U. | | 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 | [Baader, Franz]
[Lenzerini, Maurizio]
[Nutt, Werner]
[Patel-Schneider, Peter F.] | | Description Logics for Natural Language Processing
In: International Workshop on Description Logics '94, 80-84 | Proceedings Article | |
| | 1994 | Hustadt, Ullrich | Baader, Franz
Buchheit, Martin
Jeusfeld, Manfred A.
Nutt, Werner | | 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 | Bachem, A.
et al. | | 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 | [Robinson, J. A.]
[Voronkov, A.] | | Resolution Theorem Proving
In: Handbook of Automated Reasoning, 19-99 | 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 | Bibel, Wolfgang
Schmitt, Peter H. | | 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 | Kirchner, Claude
Kirchner, Hélène | | Strict Basic Superposition
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 160-174 | Proceedings Article | |
| | 1998 | Bachmair, Leo
Ganzinger, Harald
Voronkov, Andrei | Kirchner, Claude
Kirchner, Hélène | | Elimination of Equality via Transformation with Ordering Constraints
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 175-190 | Proceedings Article | |
| | 1995 | Bachmair, Leo
Ganzinger, Harald | Dershowitz, N.
Lindenstrauss, N. | | 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 | Astesiano, Egidio
Reggio, Gianna
Tarlecki, Andrzej | | 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 | |
