**Number** | | **Title** | **Name(s)** | **Pages** |

2007-2-001 | | A method and a tool for automatic veriication of region stability for hybrid systems | Podelski, Wagner | 46 |

2006-2-001 | | On verifying complex properties using symbolic shape analysis | Wies, Kuncak, Zee, Podelski, Rinard | 32 |

2005-2-004 | | A Framework of refutational theorem proving for saturation-based decision procedures | Kazakov | ? |

2005-2-003 | | Using resolution as a decision procedure | Nivelle | 53 |

2005-2-002 | | Bounded model checking of pointer programs | Maier, Charatonik, Georgieva | 34 |

2005-2-001 | | Bottleneck behavior in CNF formulas | Hoffmann, Gomes, Selman | 35 |

2004-2-007 | | Summaries for while programs with recursion | Wagner | 22 |

2004-2-002 | | Intuitionistic LTL and a new characterization of safety and liveness | Maier | 20 |

2004-2-001 | | Resolution decision procedures for the guarded fragment with transitive guards | de Nivelle, Kazakov | 32 |

2003-2-004 | | Software model checking of liveness properties via transition invariants | Podelski, Rybalchenko | 29 |

2003-2-003 | | Subsumption of concepts in $DL$ $\cal FL_0$ for (cyclic) terminologies with respect to descriptive semantics is PSPACE-complete | Kazakov, de Nivelle | 12 |

2003-2-002 | | A representation theorem and applications to measure selection and noninformative priors | Jaeger | 35 |

2003-2-001 | | Compositional circular assume-guarantee rules cannot be sound and complete | Maier | 22 |

2002-2-008 | | Atomic set constraints with projection | Charatonik, Talbot | 20 |

2002-2-007 | | Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi | Charatonik, Ganzinger | 64 |

2002-1-008 | | The factor algorithm for all-to-all communication on clusters of SMP nodes | Sanders, Träff | 8 |

2001-2-006 | | Proceeding of the Second International Workshop of the Implementation of Logics | de Nivelle, Schulz | ? 102 |

2001-2-005 | | Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators | Sofronie-Stokkermans | 41 |

2001-2-003 | | Experiments with iterative improvement algorithms on completely unimodel hypercubes | Björklund, Petersson, Vorobyov | 25 |

2001-2-001 | | Superposition and chaining for totally ordered divisible abelian groups | Waldmann | 40 |

2000-2-001 | | Short vectors of planar lattices via continued fractions | Eisenbrand | 10 |

1999-2-008 | | Cutting planes and the elementary closure in fixed dimension | Bockmayr, Eisenbrand | 12 |

1999-2-007 | | Symbolic representation of upward-closed sets | Delzanno, Raskin | 24 |

1999-2-006 | | A deductive model checking approach for hybrid systems | Nonnengart | 40 |

1999-2-005 | | Symmetries in logic programs | Wu | 44 |

1999-2-004 | | Decidable fragments of simultaneous rigid reachability | Cortier, Ganzinger, Jacquemard, Veanes | 19 |

1999-2-003 | | Cancellative superposition decides the theory of divisible torsion-free abelian groups | Waldmann | 23 |

1999-2-001 | | Automata on DAG representations of finite trees | Charatonik | 30 |

98-2-018 | | A note on the membership problem for the first elementary closure of a polyhedron | Eisenbrand | 3 |

98-2-017 | | Hybridizing concept languages | Tzakova, Blackburn | 33 |

98-2-014 | | Partisan corroboration, and shifted pairing | Gurevich, Veanes | 35 |

98-2-013 | | Rigid reachability | Ganzinger, Jacquemard, Veanes | 24 |

98-2-012 | | Model checking infinite-state systems in CLP | Delzanno, Podelski | 44 |

98-2-011 | | Equality reasoning in sequent-based calculi | Degtyarev, Voronkov | 128 |

98-2-010 | | Strategies for conformance testing | Ramangalahy | 24 |

98-2-009 | | The undecidability of the first-order theories of one step rewriting in linear canonical systems | Vorobyov | 59 |

98-2-008 | | AE-Equational theory of context unification is Co-RE-Hard | Vorobyov | 20 |

98-2-007 | | The most nonelementary theory (a direct lower bound proof) | Vorobyov | 36 |

98-2-006 | | Hybrid languages and temporal logic | Blackburn, Tzakova | 29 |

98-2-005 | | The relation between second-order unification and simultaneous rigid \sl E-unification | Veanes | 26 |

98-2-004 | | Satisfiability of Functional+Record Subtype Constraints is NP-Hard | Vorobyov | 16 |

98-2-003 | | E-unification for subsystems of S4 | Schmidt | 30 |

98-2-002 | | Unification in extensions of shallow equational theories | Jacquemard, Meyer, Weidenbach | 31 |

97-2-012 | | Elimination of equality via transformation with ordering constraints | Bachmair, Ganzinger, Voronkov | 18 |

97-2-011 | | Strict basic superposition and chaining | Bachmair, Ganzinger | 22 |

97-2-010 | | Complexity of nonrecursive logic programs with complex values | Vorobyov, Voronkov | 46 |

97-2-009 | | On the Chvátal rank of polytopes in the 0/1 cube | Bockmayr, Eisenbrand | 12 |

97-2-008 | | A unifying framework for integer and finite domain constraint programming | Bockmayr, Kasper | 24 |

97-2-007 | | Two hybrid logics | Blackburn, Tzakova | 33 |

97-2-006 | | Third-order matching in $\lambda\rightarrow$-Curry is undecidable | Vorobyov | 17 |

97-2-005 | | A theory of resolution | Bachmair, Ganzinger | 79 |

97-2-004 | | Solving set constraints for greatest models | Charatonik, Podelski | 12 |

97-2-003 | | On evaluating decision procedures for modal logic | Hustadt, Schmidt | 50 |

97-2-002 | | Resolution is a decision procedure for many propositional modal logics | Schmidt | 60 |

97-2-001 | | Labelled modal logics: quantifiers | Basin, Matthews, Viganò | 31 |

96-2-010 | | Strong skolemization | Nonnengart | 16 |

96-2-009 | | Beyond the finite in automatic hardware verification | Basin, Klarlund | 51 |

96-2-008 | | On the decision complexity of the bounded theories of trees | Vorobyov | 26 |

96-2-007 | | SCAN and systems of conditional logic | Herzig | 33 |

96-2-006 | | Natural deduction for non-classical logics | Basin, Matthews, Viganò | 44 |

96-2-005 | | Auxiliary modal operators and the characterization of modal frames | Nonnengart | 37 |

96-2-004 | | Non-symmetric rewriting | Struth | 20 |

96-2-003 | | Using algebraic specification languages for model-oriented specifications | Baumeister | 17 |

96-2-002 | | Labelled propositional modal logics: theory and practice | Basin, Matthews, Viganò | 46 |

96-2-001 | | Theorem proving in cancellative abelian monoids | Ganzinger, Waldmann | 52 |

95-2-011 | | Modelling mixed-integer optimisation problems in constraint logic programming | Barth, Bockmayr | 22 |

95-2-010 | | Special cases and substitutes for rigid $E$-unification | Plaisted | 46 |

95-2-009 | | Ordered chaining calculi for first-order theories of binary relations | Bachmair, Ganzinger | 42 |

95-2-008 | | Translating graded modalities into predicate logic | Ohlbach, Schmidt, Hustadt | 37 |

95-2-007 | | A fixpoint approach to second-order quantifier elimination with applications to correspondence theory | Nonnengart, Szalas | 16 |

95-2-006 | | Automated complexity analysis based on ordered resolution | Basin, Ganzinger | 33 |

95-2-005 | | A multi-dimensional terminological knowledge representation language | Baader, Ohlbach | 32 |

95-2-003 | | A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization | Barth | 13 |

95-2-002 | | Functional translation and second-order frame properties of modal logics | Ohlbach, Schmidt | 27 |

95-2-001 | | Proof normalization and subject reduction in extensions of Fsub | Vorobyov | 18 |

94-261 | | Finite domain and cutting plane techniques in CLP($\cal PB$) | Barth, Bockmayr | 16 |

94-257 | | Structural decidable extensions of bounded quantification | Vorobyov | 12 |

94-252 | | A survey of program transformation with special reference to unfold/fold style program development | Madden | 36 |

94-251 | | Substitution tree indexing | Graf | 34 |

94-246 | | On extra variables in (Equational) logic programming | Hanus | 33 |

94-241 | | Genetic algorithms within the framework of evolutionary computation: Proceedings of the KI-94 Workshop | Hopf (ed.) | 161 |

94-240 | | Recursive program optimization through inductive synthesis proof transformation | Madden | 44 |

94-239 | | A general technique for automatically optimizing programs through the use of proof plans | Madden, Green | 16 |

94-238 | | Formal methods of automated program improvement | Madden | 12 |

94-235 | | Ordered semantic hyper-linking | Plaisted | 22 |

94-234 | | Reflection using the derivability conditions | Matthews, Simpson | 14 |

94-233 | | The search efficiency of theorem proving strategies: an analytical comparison | Plaisted | 40 |

94-232 | | An abstract program generation logic | Plaisted | 58 |

94-230 | | Temporal logic: Proceedings of the ICTL Workshop | Ohlbach (ed.) | 116 |

94-229 | | Classical methods in nonmonotonic reasoning | Dimopoulos | 26 |

94-228 | | Computer support for the development and investigation of logics | Ohlbach | 24 |

94-227 | | Minimal resolution | Weidenbach | 20 |

94-226 | | Killer transformations | Ohlbach, Gabbay, Plaisted | 45 |

94-225 | | Synthesizing semantics for extensions of propositional logic | Ohlbach | 45 |

94-224 | | Integration of declarative paradigms: Proceedings of the ICLP'94 Post-Conference Workshop, Santa Margherita Ligure, Italy | Aït-Kaci, Hanus, Navarro | 149 |

94-223 | | LDS - Labelled Deductive Systems: Volume 1 - Foundations | Gabbay | 465 |

94-218 | | Logic frameworks for logic programs | Basin | 13 |

94-216 | | Linear 0-1 inequalities and extended clauses | Barth | 53 |

94-209 | | Termination orderings for rippling | Basin, Walsh | 15 |

94-208 | | A probabilistic extension of terminological logics | Jaeger | 64 |

94-207 | | Cutting planes in constraint logic programming | Bockmayr | 23 |

94-201 | | The integration of functions into logic programming: a survey | Hanus | 48 |

93-267 | | Associative-commutative superposition | Bachmair, Ganzinger | ? |

93-265 | | Negativ set constraints: an easy proof of decidability | Charatonik, Pacholski | 11 |

93-264 | | Graph theoretical structures in logic programs and default theories | Dimopoulos, Torres | 28 |

93-260 | | The logic of preference and decision supporting systems | Cvetkovic | 71 |

93-258 | | Linear logic meets the Lambda Calculus, part I | Tönne | ? |

93-257 | | Computing stable models by program transformation | Stuber | 15 |

93-256 | | Solving simplifications ordering constraints | Johann, Socher-Ambrosius | 16 |

93-253 | | Extended path-indexing | Graf, Meyer | ? |

93-253 | | Extended path-Indexing | Graf, Meyer | ? |

93-250 | | Ordered chaining for total orderings | Bachmair, Ganzinger | 20 |

93-249 | | Rewrite techniques for transitive relations | Bachmair, Ganzinger | 19 |

93-243 | | A needed narrowing strategy | Antoy, Echahed, Hanus | 28 |

93-237 | | A refined version of general E-unification | Socher-Ambrosius | 12 |

93-236 | | Basic paramodulation | Bachmair, Ganzinger, Lynch, Snyder | 36 |

93-235 | | A conservative extension of first-order logic and its application to theorem proving | Basin, Matthews | 11 |

93-234 | | Künstliche Intelligenz und Operations Research | Bockmayr, Radermacher | 36 |

93-233 | | Narrowing strategies for arbitrary canonical rewrite systems | Bockmayr, Krischer, Werner | 29 |

93-231 | | A framework for program development based on schematic proof | Basin, Bundy, Kraan, Matthews | 12 |

93-230 | | Classical vs non-classical logics: the universality of classical logic | Gabbay | 101 |

93-227 | | A theory and its metatheory in FS 0 | Matthews | 22 |

93-226 | | On kernels, defaults and even graphs | Dimopoulos, Magirou, Papadimitriou | 11 |

93-225 | | Translation methods for non-classical logics: an overview | Ohlbach | 18 |

93-222 | | A debugging model for functional logic programs | Hanus, Josephs | 14 |

93-220 | | Towards automating duality | Brink, Gabbay, Ohlbach | 50 |

93-217 | | Unification of terms with exponents | Socher-Ambrosius | 21 |

93-215 | | Lazy unification with inductive simplification | Hanus | 20 |

93-214 | | Middle-out reasoning for logic program synthesis | Basin, Kraan, Bundy | 12 |

93-213 | | Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Marseille, France, 1993 | Basin, Hähnle, Fronhöfer, Posegga, Schwind (ed.) | |

93-212 | | A multi-dimensional terminological knowledge representation language - preliminary version | Ohlbach, Baader | 17 |

93-211 | | Unification in sort theories and its applications | Weidenbach | 36 |

93-204 | | Superposition with simplification as a decision procedure for the monadic class with equality | Ganzinger, Bachmair, Waldmann | 14 |

92-251 | | Analysis of nonlinear constraints in CLP(R) | Hanus | 31 |

92-250 | | Reflection in logical systems | Matthews | 14 |

92-247 | | Difference unification | Basin, Walsh | 15 |

92-246 | | Terminological representation, natural language & relation algebra | Schmidt | 13 |

92-244 | | Logic program synthesis via proof planning | Kraan, Basin, Bundy | 14 |

92-242 | | Temporal logic: Mathematical foundations, part 2 | Gabbay, Hodkinson, Reynolds | 30 |

92-240 | | Set constraints are the Monadic class | Ganzinger, Bachmair, Waldmann | 13 |

92-238 | | A new ordering constraint solving method and its applications | Nieuwenhuis | 12 |

92-237 | | Path indexing for term retrieval | Graf | 12 |

92-236 | | Motel user manual | Hustadt, Nonnengart, Schmidt, Timm | 45 |

92-233 | | CLP($\cal PB$): A Meta-Interpreter in CLP($\cal R$) | Barth | 18 |

92-232 | | Preprints of Proceedings of GWAI-92 | Ohlbach | 47 |

92-231 | | Quantifier elimination in second-order predicate logic | Gabbay, Ohlbach | 18 |

92-230 | | A recursion planning analysis of inductive completion | Barnett, Basin, Hesketh | 14 |

92-229 | | Peirce algebras | Brink, Britz, Schmidt | 22 |

92-228 | | First-order modal logic theorem proving and standard PROLOG | Nonnengart | 48 |

92-224 | | Completeness of resolution and superposition calculi | Socher-Ambrosius | 9 |

92-219 | | Unification and matching in Church's Original Lambda Calculus | Hustadt | 16 |

92-217 | | An abstract interpretation algorithm for residuating logic programs | Hanus | 20 |

92-216 | | First-order theorem proving modulo equations | Wertz | 108 |

92-214 | | Experience with FS0 as a framework theory | Matthews, Smaill, Basin | 25 |

92-213 | | Temporal logic: Mathematical foundations | Gabbay | 166 |

92-211 | | Difference matching | Basin, Walsh | 12 |

92-209 | | On correspondence between modal and classical logic: automated approach | Szalas | 17 |

92-207 | | Semi-unification | Socher-Ambrosius | 10 |

92-206 | | A goal oriented strategy based on completion | Socher-Ambrosius | 14 |

92-205 | | Metalogical frameworks | Basin, Constable | 20 |

92-203 | | On natural deduction in fixpoint logics | Szalas | 18 |

91-228 | | A complete transformation system for polymorphic higher-order unification | Hustadt | 22 |

91-227 | | Logic programming with pseudo-Boolean constraints | Bockmayr | 20 |

91-218 | | A sorted logic using dynamic sorts | Weidenbach | 71 |

91-217 | | Deduction systems based on resolution | Eisinger, Ohlbach | 68 |

91-216 | | Algebraic terminological representation | Schmidt | 113 |

91-211 | | Natural semantics and some of its meta-theory in Elf | Michaylov, Pfenning | 26 |

91-209 | | Associative-commutative reduction orderings | Bachmair | 7 |

91-208 | | Rewrite-based equational theorem proving with selection and simplification | Bachmair, Ganzinger | 24 |