MPI-INF/SWS Research Reports 1991-2021

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

2007-2-001Attachment IconA method and a tool for automatic veriication of region stability for hybrid systemsPodelski, Wagner46
2006-2-001Attachment IconOn verifying complex properties using symbolic shape analysisWies, Kuncak, Zee, Podelski, Rinard32
2005-2-004A Framework of refutational theorem proving for saturation-based decision proceduresKazakov?
2005-2-003Attachment IconUsing resolution as a decision procedureNivelle53
2005-2-002Attachment IconBounded model checking of pointer programsMaier, Charatonik, Georgieva34
2005-2-001Attachment IconBottleneck behavior in CNF formulasHoffmann, Gomes, Selman35
2004-2-007Attachment IconSummaries for while programs with recursionWagner22
2004-2-002Attachment IconIntuitionistic LTL and a new characterization of safety and livenessMaier20
2004-2-001Attachment IconResolution decision procedures for the guarded fragment with transitive guardsde Nivelle, Kazakov32
2003-2-004Attachment IconSoftware model checking of liveness properties via transition invariantsPodelski, Rybalchenko29
2003-2-003Attachment IconSubsumption of concepts in $DL$ $\cal FL_0$ for (cyclic) terminologies with respect to descriptive semantics is PSPACE-completeKazakov, de Nivelle12
2003-2-002Attachment IconA representation theorem and applications to measure selection and noninformative priorsJaeger35
2003-2-001Attachment IconCompositional circular assume-guarantee rules cannot be sound and completeMaier22
2002-2-008Attachment IconAtomic set constraints with projectionCharatonik, Talbot20
2002-2-007Attachment IconSymposium on the Effectiveness of Logic in Computer Science in Honour of Moshe VardiCharatonik, Ganzinger64
2002-1-008Attachment IconThe factor algorithm for all-to-all communication on clusters of SMP nodesSanders, Träff8
2001-2-006Attachment IconProceeding of the Second International Workshop of the Implementation of Logicsde Nivelle, Schulz? 102
2001-2-005Attachment IconResolution-based decision procedures for the universal theory of some classes of distributive lattices with operatorsSofronie-Stokkermans41
2001-2-003Attachment IconExperiments with iterative improvement algorithms on completely unimodel hypercubesBjörklund, Petersson, Vorobyov25
2001-2-001Attachment IconSuperposition and chaining for totally ordered divisible abelian groupsWaldmann40
2000-2-001Attachment IconShort vectors of planar lattices via continued fractionsEisenbrand10
1999-2-008Attachment IconCutting planes and the elementary closure in fixed dimensionBockmayr, Eisenbrand12
1999-2-007Attachment IconSymbolic representation of upward-closed setsDelzanno, Raskin24
1999-2-006Attachment IconA deductive model checking approach for hybrid systemsNonnengart40
1999-2-005Attachment IconSymmetries in logic programsWu44
1999-2-004Attachment IconDecidable fragments of simultaneous rigid reachabilityCortier, Ganzinger, Jacquemard, Veanes19
1999-2-003Attachment IconCancellative superposition decides the theory of divisible torsion-free abelian groupsWaldmann23
1999-2-001Attachment IconAutomata on DAG representations of finite treesCharatonik30
98-2-018Attachment IconA note on the membership problem for the first elementary closure of a polyhedronEisenbrand3
98-2-017Attachment IconHybridizing concept languagesTzakova, Blackburn33
98-2-014Attachment IconPartisan corroboration, and shifted pairingGurevich, Veanes35
98-2-013Attachment IconRigid reachabilityGanzinger, Jacquemard, Veanes24
98-2-012Attachment IconModel checking infinite-state systems in CLPDelzanno, Podelski44
98-2-011Attachment IconEquality reasoning in sequent-based calculiDegtyarev, Voronkov128
98-2-010Attachment IconStrategies for conformance testingRamangalahy24
98-2-009Attachment IconThe undecidability of the first-order theories of one step rewriting in linear canonical systemsVorobyov59
98-2-008Attachment IconAE-Equational theory of context unification is Co-RE-HardVorobyov20
98-2-007Attachment IconThe most nonelementary theory (a direct lower bound proof)Vorobyov36
98-2-006Attachment IconHybrid languages and temporal logicBlackburn, Tzakova29
98-2-005Attachment IconThe relation between second-order unification and simultaneous rigid \sl E-unificationVeanes26
98-2-004Attachment IconSatisfiability of Functional+Record Subtype Constraints is NP-HardVorobyov16
98-2-003Attachment IconE-unification for subsystems of S4Schmidt30
98-2-002Attachment IconUnification in extensions of shallow equational theoriesJacquemard, Meyer, Weidenbach31
97-2-012Attachment IconElimination of equality via transformation with ordering constraintsBachmair, Ganzinger, Voronkov18
97-2-011Attachment IconStrict basic superposition and chainingBachmair, Ganzinger22
97-2-010Attachment IconComplexity of nonrecursive logic programs with complex valuesVorobyov, Voronkov46
97-2-009Attachment IconOn the Chvátal rank of polytopes in the 0/1 cubeBockmayr, Eisenbrand12
97-2-008Attachment IconA unifying framework for integer and finite domain constraint programmingBockmayr, Kasper24
97-2-007Attachment IconTwo hybrid logicsBlackburn, Tzakova33
97-2-006Attachment IconThird-order matching in $\lambda\rightarrow$-Curry is undecidableVorobyov17
97-2-005Attachment IconA theory of resolutionBachmair, Ganzinger79
97-2-004Attachment IconSolving set constraints for greatest modelsCharatonik, Podelski12
97-2-003Attachment IconOn evaluating decision procedures for modal logicHustadt, Schmidt50
97-2-002Attachment IconResolution is a decision procedure for many propositional modal logicsSchmidt60
97-2-001Attachment IconLabelled modal logics: quantifiersBasin, Matthews, Viganò31
96-2-010Attachment IconStrong skolemizationNonnengart16
96-2-009Attachment IconBeyond the finite in automatic hardware verificationBasin, Klarlund51
96-2-008Attachment IconOn the decision complexity of the bounded theories of treesVorobyov26
96-2-007Attachment IconSCAN and systems of conditional logicHerzig33
96-2-006Attachment IconNatural deduction for non-classical logicsBasin, Matthews, Viganò44
96-2-005Attachment IconAuxiliary modal operators and the characterization of modal framesNonnengart37
96-2-004Attachment IconNon-symmetric rewritingStruth20
96-2-003Attachment IconUsing algebraic specification languages for model-oriented specificationsBaumeister17
96-2-002Attachment IconLabelled propositional modal logics: theory and practiceBasin, Matthews, Viganò46
96-2-001Attachment IconTheorem proving in cancellative abelian monoidsGanzinger, Waldmann52
95-2-011Attachment IconModelling mixed-integer optimisation problems in constraint logic programmingBarth, Bockmayr22
95-2-010Attachment IconSpecial cases and substitutes for rigid $E$-unificationPlaisted46
95-2-009Attachment IconOrdered chaining calculi for first-order theories of binary relationsBachmair, Ganzinger42
95-2-008Attachment IconTranslating graded modalities into predicate logicOhlbach, Schmidt, Hustadt37
95-2-007Attachment IconA fixpoint approach to second-order quantifier elimination with applications to correspondence theoryNonnengart, Szalas16
95-2-006Attachment IconAutomated complexity analysis based on ordered resolutionBasin, Ganzinger33
95-2-005Attachment IconA multi-dimensional terminological knowledge representation languageBaader, Ohlbach32
95-2-003Attachment IconA Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimizationBarth13
95-2-002Attachment IconFunctional translation and second-order frame properties of modal logicsOhlbach, Schmidt27
95-2-001Attachment IconProof normalization and subject reduction in extensions of FsubVorobyov18
94-261Attachment IconFinite domain and cutting plane techniques in CLP($\cal PB$)Barth, Bockmayr16
94-257Attachment IconStructural decidable extensions of bounded quantificationVorobyov12
94-252Attachment IconA survey of program transformation with special reference to unfold/fold style program developmentMadden36
94-251Attachment IconSubstitution tree indexingGraf34
94-246Attachment IconOn extra variables in (Equational) logic programmingHanus33
94-241Attachment IconGenetic algorithms within the framework of evolutionary computation: Proceedings of the KI-94 WorkshopHopf (ed.)161
94-240Attachment IconRecursive program optimization through inductive synthesis proof transformationMadden44
94-239Attachment IconA general technique for automatically optimizing programs through the use of proof plansMadden, Green16
94-238Attachment IconFormal methods of automated program improvementMadden12
94-235Attachment IconOrdered semantic hyper-linkingPlaisted22
94-234Attachment IconReflection using the derivability conditionsMatthews, Simpson14
94-233Attachment IconThe search efficiency of theorem proving strategies: an analytical comparisonPlaisted40
94-232Attachment IconAn abstract program generation logicPlaisted58
94-230Attachment IconTemporal logic: Proceedings of the ICTL WorkshopOhlbach (ed.)116
94-229Attachment IconClassical methods in nonmonotonic reasoningDimopoulos26
94-228Attachment IconComputer support for the development and investigation of logicsOhlbach24
94-227Attachment IconMinimal resolutionWeidenbach20
94-226Attachment IconKiller transformationsOhlbach, Gabbay, Plaisted45
94-225Attachment IconSynthesizing semantics for extensions of propositional logicOhlbach45
94-224Attachment IconIntegration of declarative paradigms: Proceedings of the ICLP'94 Post-Conference Workshop, Santa Margherita Ligure, ItalyAït-Kaci, Hanus, Navarro149
94-223Attachment IconLDS - Labelled Deductive Systems: Volume 1 - FoundationsGabbay465
94-218Attachment IconLogic frameworks for logic programsBasin13
94-216Attachment IconLinear 0-1 inequalities and extended clausesBarth53
94-209Attachment IconTermination orderings for ripplingBasin, Walsh15
94-208Attachment IconA probabilistic extension of terminological logicsJaeger64
94-207Attachment IconCutting planes in constraint logic programming Bockmayr23
94-201Attachment IconThe integration of functions into logic programming: a surveyHanus48
93-267Attachment IconAssociative-commutative superpositionBachmair, Ganzinger?
93-265Attachment IconNegativ set constraints: an easy proof of decidabilityCharatonik, Pacholski11
93-264Attachment IconGraph theoretical structures in logic programs and default theoriesDimopoulos, Torres28
93-260Attachment IconThe logic of preference and decision supporting systemsCvetkovic71
93-258Linear logic meets the Lambda Calculus, part ITönne?
93-257Attachment IconComputing stable models by program transformationStuber15
93-256Attachment IconSolving simplifications ordering constraintsJohann, Socher-Ambrosius16
93-253Attachment IconExtended path-indexingGraf, Meyer?
93-253Attachment IconExtended path-IndexingGraf, Meyer?
93-250Attachment IconOrdered chaining for total orderingsBachmair, Ganzinger20
93-249Attachment IconRewrite techniques for transitive relationsBachmair, Ganzinger19
93-243Attachment IconA needed narrowing strategyAntoy, Echahed, Hanus28
93-237Attachment IconA refined version of general E-unificationSocher-Ambrosius12
93-236Attachment IconBasic paramodulationBachmair, Ganzinger, Lynch, Snyder36
93-235Attachment IconA conservative extension of first-order logic and its application to theorem provingBasin, Matthews11
93-234Attachment IconKünstliche Intelligenz und Operations ResearchBockmayr, Radermacher36
93-233Attachment IconNarrowing strategies for arbitrary canonical rewrite systemsBockmayr, Krischer, Werner29
93-231Attachment IconA framework for program development based on schematic proofBasin, Bundy, Kraan, Matthews12
93-230Attachment IconClassical vs non-classical logics: the universality of classical logicGabbay101
93-227Attachment IconA theory and its metatheory in FS 0Matthews22
93-226Attachment IconOn kernels, defaults and even graphsDimopoulos, Magirou, Papadimitriou11
93-225Attachment IconTranslation methods for non-classical logics: an overviewOhlbach18
93-222Attachment IconA debugging model for functional logic programsHanus, Josephs14
93-220Attachment IconTowards automating dualityBrink, Gabbay, Ohlbach50
93-217Attachment IconUnification of terms with exponentsSocher-Ambrosius21
93-215Attachment IconLazy unification with inductive simplificationHanus20
93-214Attachment IconMiddle-out reasoning for logic program synthesisBasin, Kraan, Bundy12
93-213Attachment IconWorkshop on Theorem Proving with Analytic Tableaux and Related Methods, Marseille, France, 1993Basin, Hähnle, Fronhöfer, Posegga, Schwind (ed.)?
93-212Attachment IconA multi-dimensional terminological knowledge representation language - preliminary versionOhlbach, Baader17
93-211Attachment IconUnification in sort theories and its applicationsWeidenbach36
93-204Attachment IconSuperposition with simplification as a decision procedure for the monadic class with equalityGanzinger, Bachmair, Waldmann14
92-251Attachment IconAnalysis of nonlinear constraints in CLP(R)Hanus31
92-250Attachment IconReflection in logical systemsMatthews14
92-247Attachment IconDifference unificationBasin, Walsh15
92-246Attachment IconTerminological representation, natural language & relation algebraSchmidt13
92-244Attachment IconLogic program synthesis via proof planningKraan, Basin, Bundy14
92-242Attachment IconTemporal logic: Mathematical foundations, part 2Gabbay, Hodkinson, Reynolds30
92-240Attachment IconSet constraints are the Monadic classGanzinger, Bachmair, Waldmann13
92-238Attachment IconA new ordering constraint solving method and its applicationsNieuwenhuis12
92-237Attachment IconPath indexing for term retrievalGraf12
92-237Attachment IconPath Indexing for Term RetrievalGraf12
92-236Attachment IconMotel user manualHustadt, Nonnengart, Schmidt, Timm45
92-236Attachment IconMotel User ManualHustadt, Nonnengart, Schmidt, Timm
92-236Attachment IconMotel User ManualHustadt, Nonnengart, Schmidt, Timm
92-233Attachment IconCLP($\cal PB$): A Meta-Interpreter in CLP($\cal R$)Barth18
92-232Attachment IconPreprints of Proceedings of GWAI-92Ohlbach47
92-231Attachment IconQuantifier elimination in second-order predicate logicGabbay, Ohlbach18
92-230Attachment IconA recursion planning analysis of inductive completionBarnett, Basin, Hesketh14
92-229Attachment IconPeirce algebrasBrink, Britz, Schmidt22
92-228Attachment IconFirst-order modal logic theorem proving and standard PROLOGNonnengart48
92-224Attachment IconCompleteness of resolution and superposition calculiSocher-Ambrosius9
92-219Attachment IconUnification and matching in Church's Original Lambda CalculusHustadt16
92-217Attachment IconAn abstract interpretation algorithm for residuating logic programsHanus20
92-216Attachment IconFirst-order theorem proving modulo equationsWertz108
92-214Attachment IconExperience with FS0 as a framework theoryMatthews, Smaill, Basin25
92-213Attachment IconTemporal logic: Mathematical foundationsGabbay166
92-211Attachment IconDifference matchingBasin, Walsh12
92-209Attachment IconOn correspondence between modal and classical logic: automated approachSzalas17
92-207Attachment IconSemi-unificationSocher-Ambrosius10
92-206Attachment IconA goal oriented strategy based on completionSocher-Ambrosius14
92-205Attachment IconMetalogical frameworksBasin, Constable20
92-203Attachment IconOn natural deduction in fixpoint logicsSzalas18
91-228Attachment IconA complete transformation system for polymorphic higher-order unificationHustadt22
91-227Attachment IconLogic programming with pseudo-Boolean constraintsBockmayr20
91-218Attachment IconA sorted logic using dynamic sortsWeidenbach71
91-217Attachment IconDeduction systems based on resolutionEisinger, Ohlbach68
91-216Attachment IconAlgebraic terminological representationSchmidt113
91-211Attachment IconNatural semantics and some of its meta-theory in ElfMichaylov, Pfenning26
91-209Attachment IconAssociative-commutative reduction orderingsBachmair7
91-208Attachment IconRewrite-based equational theorem proving with selection and simplificationBachmair, Ganzinger24