2. Number - only D2

MPI-INF/SWS Research Reports 1991-2021

2. Number - only D2 - MPI-INF/SWS Research Reports 1991-2021

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-237	Path Indexing for Term Retrieval	Graf	12
92-236	Motel user manual	Hustadt, Nonnengart, Schmidt, Timm	45
92-236	Motel User Manual	Hustadt, Nonnengart, Schmidt, Timm
92-236	Motel User Manual	Hustadt, Nonnengart, Schmidt, Timm
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

Imprint / Impressum | Data Protection / Datenschutzhinweis