BibTeX cite key | Author/Editor | Year | | Title | Type |
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 |
BachmairGanzingerWaldmann-92-alp | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | 1992 | | Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434 | Proceedings Article |
BachmairGanzingerWaldmann-93-kgs | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | 1993 | | Superposition with simplification as a decision procedure for the monadic class with equality
In: Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC'93, 83-96 | Proceedings Article |
BachmairGanzingerWaldmann-93-lics | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | 1993 | | Set Constraints are the Monadic Class
In: Eighth Annual IEEE Symposium on Logic in Computer Science, 75-83 | Proceedings Article |
BachmairGanzingerWaldmann-94-aaecc | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | 1994 | | Refutational Theorem Proving for Hierarchic First-Order Theories
In: Applicable Algebra in Engineering, Communication and Computing (AAECC) [5], 193-212 | Journal Article |
BackesDiss2005 | Backes, Werner | 2005 | | Programmanalyse des XRTL Zwischencodes
Universität des Saarlandes | Thesis - PhD thesis |
BallPodelskiRajamaniTACAS2000 | Ball, Thomas
Podelski, Andreas
Rajamani, Sriram K. | 2001 | | Boolean and Cartesian Abstraction for Model Checking C Programs
In: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2001), 268-283 | Proceedings Article |
BarnettBasinHesketh92a | Barnett, Richard
Basin, David A.
Hesketh, Jane | 1993 | | A Recursion Planning Analysis of Inductive Completion
In: Annals of Mathematics and Artificial Intelligence [8], 363-381 | Journal Article |
Barth-95b | Barth, Peter | 1995 | | Logic-based 0-1 constraint programming | Book |
Barth-Diss | Barth, Peter | 1995 | | Logic-based 0-1 Constraint Solving in Constraint Logic Programming
Fachbereich Informatik, Universität des Saarlandes, Germany | Thesis - PhD thesis |
Barth93b | Barth, Peter | 1993 | | Linear 0-1 Inequalities and Extended Clauses
In: Proceedings~4th International~Conference on Logic Programming and Automated Reasoning LPAR '93, 40-51 | Proceedings Article |
Barth93c | Barth, Peter | 1993 | | A Complete Symbolic 0-1 Constraint Solver
In: 3rd Workshop on Constraint Logic Programming (WCLP '93), ? | Proceedings Article |
Barth94a | Barth, Peter | 1994 | | Simplifying Clausal Satisfiability Problems
In: Proceedings of the 1st International Conference on Constraints in Computational Logics (CCL'94), 19-33 | Proceedings Article |