| BibTeX cite key | Author/Editor | Year | | Title | Type |
|---|
| Abdu95 | Ayari, Abdelwaheb | 1995 |  | A Reinterpretation of the Deductive Tableaux System in Higher-Order Logic
Universität des Saarlandes | Thesis - Masters thesis |
| AbduBasin-TACAS96 | Ayari, Abdelwaheb
Basin, David A. | 1996 | | 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 |
| AfshordelHillenbrandWeidenbach01 | Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph | 2001 | | First-Order Atom Definitions Extended
In: Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001), 309-319 | Proceedings Article |
| Althaus-Diplom98 | Althaus, Ernst | 1998 | | Berechnung optimaler Steinerbäume in der Ebene
Universität des Saarlandes | Thesis - Masters thesis |
| AmadioCharatonik2002 | Charatonik, Witold
Amadio, Roberto | 2002 | | On Name Generation and Set-Based Analysis in the Dolev-Yao Model
In: CONCUR 2002 - Concurrency Theory. 13th International Conference, 499-514 | Proceedings Article |
| Anderson&Basin | Anderson, Penny
Basin, David A. | 1995 | | Deriving and Applying Logic Program Transformers
In: Algorithms, Concurrency and Knowledge (1995 Asian Computing Science Conference), 301-318 | Proceedings Article |
| AntoyEchahedHanus94a | Antoy, Sergio
Echahed, Rachid
Hanus, Michael | 1994 | | A Needed Narrowing Strategy
In: Proceedings of the 21st ACM Symposium on Principles of Programming Languages (POPL'94), 268-279 | Proceedings Article |
| ArecesRijkeNivelle02 | Areces, Carlos
de Rijke, Maarten
de Nivelle, Hans | 2001 | | Resolution in modal, description and hybrid logic
In: Journal of Logic and Computation [11], 717-736 | Journal Article |
| ArgonEtAlSofSem2001 | Argon, Pablo
Delzanno, Giorgio
Mukhopadhyay, Supratik
Podelski, Andreas | 2001 | | Model Checking for Communication Protocols
In: Proceedings of the 28th Annual Conference on Current Trends in Theory and Practice of Informatics (SOFSEM-2001), 160-170 | Proceedings Article |
| AutexierDipl96 | Autexier, Serge | 1996 | | Heuristiken zum Beweisen von Gleichungen
Universität des Saarlandes | Thesis - Masters thesis |
| AvenhausHillenbrandLoechner2003 | Avenhaus, Jürgen
Hillenbrand, Thomas
Löchner, Bernd | 2003 | | On Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233 | Journal Article |
| AyariBasin2001 | Ayari, Abdelwaheb
Basin, David A. | 2001 | | A Higher-order Interpretation of Deductive Tableau
In: Journal of Symbolic Computation [31], 487-520 | Journal Article |
| BaaderOhlbach95 | Baader, Franz
Ohlbach, Hans Jürgen | 1995 | | A Multi-Dimensional Terminological Knowledge Representation Language
In: Journal of Applied Non-Classical Logics [5], 153-198 | Journal Article |
| Bach96 | Bach, Alexander | 1996 | | Static analysis of functional programs via Linear Logic
Universität des Saarlandes | Thesis - Masters thesis |
| Bachmair-et-al-92-cade | Bachmair, Leo
Ganzinger, Harald
Lynch, Christopher
Snyder, Wayne | 1992 | | Basic Paramodulation and Superposition
In: Proceedings of the 11th International Conference on Automated Deduction (CADE-11), 462-476 | Proceedings Article |
| Bachmair-et-al-95-ic | Bachmair, Leo
Ganzinger, Harald
Lynch, Christopher
Snyder, Wayne | 1995 | | Basic Paramodulation
In: Information and Computation [121], 172-192 | Journal Article |
| BachmairGanzinger-01-har | Bachmair, Leo
Ganzinger, Harald | 2001 | | Resolution Theorem Proving
In: Handbook of Automated Reasoning, 19-99 | Part of a Book |
| BachmairGanzinger-91-ctrs | Bachmair, Leo
Ganzinger, Harald | 1991 | | Completion of first-order clauses with equality by strict superposition
In: Proceedings of the 2nd International Workshop on Conditional and Typed Rewriting, 162-180 | Proceedings Article |
| BachmairGanzinger-91-iclp | Bachmair, Leo
Ganzinger, Harald | 1991 | | Perfect model semantics for logic programs with equality
In: Proceedings International Conference on Logic Programming '91, 645-659 | Proceedings Article |
| BachmairGanzinger-92-lpar | Bachmair, Leo
Ganzinger, Harald | 1992 | | Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria
In: Logic Programming and Automated Reasoning, 273-284 | Proceedings Article |
| BachmairGanzinger-94-cade | Bachmair, Leo
Ganzinger, Harald | 1994 | | Ordered Chaining for Total Orderings
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 435-450 | Proceedings Article |
| BachmairGanzinger-94-ccl | Bachmair, Leo
Ganzinger, Harald | 1994 | | Buchberger's algorithm: a constraint-based completion procedure
In: Proceedings of the 1st International Conference on Constraints in Computational Logics (CCL'94), 285-301 | Proceedings Article |
| BachmairGanzinger-94-jlc | Bachmair, Leo
Ganzinger, Harald | 1994 | | Rewrite-based equational theorem proving with selection and simplification
In: Journal of Logic and Computation [4], 217-247 | Journal Article |
| BachmairGanzinger-94-lics | Bachmair, Leo
Ganzinger, Harald | 1994 | | Rewrite Techniques for Transitive Relations
In: Proceedings of the 9th IEEE Symposium on Logic in Computer Science, 384-393 | Proceedings Article |
| BachmairGanzinger-95-ctrs | Bachmair, Leo
Ganzinger, Harald | 1995 | | Associative-Commutative Superposition
In: Proceedings of the 4th International Workshop on Conditional and Typed Rewrite Systems (CTRS-94), 1-14 | Proceedings Article |
| BachmairGanzinger-98-cade | Bachmair, Leo
Ganzinger, Harald | 1998 | | Strict Basic Superposition
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 160-174 | Proceedings Article |
| BachmairGanzinger-98-jacm | Bachmair, Leo
Ganzinger, Harald | 1998 | | Ordered Chaining Calculi for First-Order Theories of Transitive Relations
In: Journal of the ACM [45], 1007-1049 | Journal Article |
| BachmairGanzinger-98-sppd | Bachmair, Leo
Ganzinger, Harald | 1998 | | Equational Reasoning in Saturation-Based Theorem Proving
In: Automated Deduction: A Basis for Applications, 353-397 | Part of a Book |
| BachmairGanzingerStuber-95-compass | Bachmair, Leo
Ganzinger, Harald
Stuber, Jürgen | 1995 | | 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 |
| BachmairGanzingerVoronkov-98-cade | Bachmair, Leo
Ganzinger, Harald
Voronkov, Andrei | 1998 | | Elimination of Equality via Transformation with Ordering Constraints
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 175-190 | Proceedings Article |
