Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

Publications Master Template

Publications Master Template

Entries sorted by: 5. Year - 8. Counting Publications

Login to this database


 

Previous Page | Next Page | Expand All | Collapse All | Search (Full Text)
Show entries starting with: A B C D E F G H I J K L M N O P Q R S T U V W X Y Z

#YAuthor/EditorTitle
1
Hide details for Thesis - Masters thesisThesis - Masters thesis
Brahm, UweMöglichkeiten des Groupware-Einsatzes im Umfeld des Wissenschaftlerarbeitsplatzes am Beispiel des Max-Planck-Instituts für Informatik
Universität des Saarlandes
2
Hide details for 20092009
1
Hide details for Proceedings ArticleProceedings Article
Meter, PeterJust a test entry
In: Booktitle, 1001-1010
1
Hide details for Journal ArticleJournal Article
Lee, Chin SoonRanking functions for size-change termination
In: ACM Transactions on Programming Languages and Systems [31], 10:1-10:42
16
Hide details for 20072007
8
Hide details for Proceedings ArticleProceedings Article
Beyer, Dirk
Henzinger, Thomas
Majumdar, Rupak
Rybalchenko, Andrey
Invariant Synthesis for Combined Theories
In: Verification, Model Checking, and Abstract Interpretation : 8th International Conference, VMCAI 2007, 378-394
Beyer, Dirk
Henzinger, Thomas
Majumdar, Rupak
Rybalchenko, Andrey
Attachment IconPath Invariants
In: PLDI'07 : Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 300-309
Cook, Byron
Gotsman, Alexey
Podelski, Andreas
Rybalchenko, Andrey
Vardi, Moshe
Proving that programs eventually do something good
In: 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), 265-276
Cook, Byron
Podelski, Andreas
Rybalchenko, Andrey
Attachment IconProving Thread Termination
In: PLDI'07 : Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 320-330
Podelski, Andreas
Rybalchenko, Andrey
Attachment IconARMC: The Logical Choice for Software Model Checking with Abstraction Refinement
In: Practical aspects of declarative languages : 9th International Symposium, PADL 2007, 245-259
Rybalchenko, AndreyPrecise Thread-Modular Verification
In: 14th International Static Analysis Symposium (SAS 2007), ?
Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica
Constraint Solving for Interpolation
In: 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007), ?
Wagner, Silke
Podelski, Andreas
Region Stability Proofs for Hybrid Systems
In: Formal Modelling and Analysis of Timed Systems: 5th International Conference, FORMATS 2007, 16
1
Hide details for PosterPoster
Podelski, Andreas
Wagner, Silke
Attachment IconA Sound and Complete Proof Rule for Region Stability of Hybrid Systems
In: Hybrid systems: computation and control : 10th International Conference, HSCC 2007, 750-753
5
Hide details for Journal ArticleJournal Article
Ben-Amram, Amir M.
Lee, Chin Soon
Program termination analysis in polynomial time
In: ACM Transactions on Programming Languages and Systems [29], 5:1-37
Podelski, Andreas
Rybalchenko, Andrey
Transition Predicate Abstraction and Fair Termination
In: ACM Transactions on Programming Languages and Systems [29], 30
Ratschan, Stefan
She, Zhikun
Attachment IconSafety Verification of Hybrid Systems by Constraint Propagation Based Abstraction Refinement
In: ACM Transactions in Embedded Computing Systems [6], 1-23
Sofronie-Stokkermans, VioricaAttachment IconAutomated theorem proving by resolution in non-classic logics
In: Discrete Applied Mathematics [?], ?
Sofronie-Stokkermans, VioricaAttachment IconOn unification for bounded distributive lattices
In: ACM Transactions on Computational Logic [8], ?
1
Hide details for Electronic Journal ArticleElectronic Journal Article
Jacobs, Swen
Sofronie-Stokkermans, Viorica
Applications of hierarchical reasoning in the verification of complex systems
In: Electronic Notes in Theoretical Computer Science [??],
1
Hide details for ReportReport
Podelski, Andreas
Wagner, Silke
Attachment IconA Method and a Tool for Automatic Verification of Region Stability for Hybrid Systems
43
Hide details for 20062006
1
Hide details for Electronic ProceedingsElectronic Proceedings
Ahrendt, Baumgartner, de Nivelle (ed.)IJCAR'06 Workshop : Disproving'06: Non-Theorems, Non-Validity, Non-Provability
25
Hide details for Proceedings ArticleProceedings Article
Cook, Byron
Podelski, Andreas
Rybalchenko, Andrey
Termination Proofs for Systems Code
In: PLDI 2006 : Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, 415-426
In: ACM SIGPLAN Notices [41], 415-426
Cook, Byron
Podelski, Andreas
Rybalchenko, Andrey
Terminator: Beyond Safety
In: Computer aided verification : 18th International Conference, CAV 2006, 415-418
Damm, Werner
Disch, Stefan
Hungar, Hardi
Pang, Jun
Pigorsch, Florian
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris
Automatic Verification of Hybrid Systems with Large Discrete State Space
In: Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, 276-291
de Nivelle, Hans
Meng, Jia
Geometric Resolution: A Proof Procedure Based on Finite Model Search
In: Automated reasoning : Third International Joint Conference, IJCAR 2006, 303-317
Domshlak, Carmel
Hoffmann, Jörg
Fast Probabilistic Planning Through Weighted Model Counting
In: Proceedings of the Sixteenth International Conference on Automated Planning and Scheduling (ICAPS 2006), 243-252
Dräge, Klaus
Finkbeiner, Bernd
Podelski, Andreas
Directed Model Checking with Distance-Preserving Abstractions
In: Model checking software : 13th International SPIN Workshop, 19-34
Freiheit, Jörn
Zangl, Fabrice
Model-based user-interface management for public services
In: 6th European Conference on e-Government, 141-151
Ganzinger, Harald
Korovin, Konstantin
Theory Instantiation
In: 13th Conference on Logic for Programming Artificial Intelligence Reasoning (LPAR'06), 497-511
Ganzinger, Harald
Korovin, Konstantin
Theory Instantiation
In: Logic for Programming, Artificial Intelligence, and Reasoning : 13th International Conference, LPAR 2006, 497-511
Hoffmann, Jörg
Gomes, Carla
Selman, Bart
Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning
In: Proceedings of the Sixteenth International Conference on Automated Planning and Scheduling (ICAPS 2006), 284-293
Hoffmann, Jörg
Sabharwal, Ashish
Domshlak, Carmel
Friends or Foes? An AI Planning Perspective on Abstraction and Search
In: Proceedings of the Sixteenth International Conference on Automated Planning and Scheduling (ICAPS 2006), 294-303
Kupferschmid, Sebastian
Hoffmann, Jörg
Dierks, Henning
Behrmann, Gerd
Adapting an AI Planning Heuristic for Directed Model Checking
In: Model checking software : 13th International SPIN Workshop, 35-52
Lilith, Nimrod
Billington, Jonathan
Freiheit, Jörn
Approximate Closed-Form Aggregation of a Fork-Join Structure in Generalised Stochastic Petri Nets
In: 1st International Conference on Performance Evaluation Methodologies and Tools, ??-??
Malkis, Alexander
Podelski, Andreas
Rybalchenko, Andrey
Thread-Modular Verification is Cartesian Abstract Interpretation
In: Theoretical Aspects of Computing - ICTAC 2006 : Third International Colloquium, 183-197
Meyer, Roland
Faber, Johannes
Rybalchenko, Andrey
Model checking Duration Calculus: a practical approach
In: Theoretical Aspects of Computing - ICTAC 2006 : Third International Colloquium, 332-346
Podelski, Andreas
Wagner, Silke
Model Checking of Hybrid Systems: From Reachability towards Stability
In: Hybrid Systems: Computation and Control : 9th International Workshop, HSCC 2006
, 507-521
Prevosto, Virgile
Waldmann, Uwe
SPASS+T
In: ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 18-33
Ratschan, Stefan
She, Zhikun
Constraints for Continuous Reachability in the Verification of Hybrid Systems
In: Artificial Intelligence and Symbolic Computation, 8th International Conference, AISC 2006, 196-210
Ratschan, Stefan
Smaus, Jan-Georg
Verification-Integrated Falsification of Non-Deterministic Hybrid Systems
In: 2nd IFAC Conference on Analysis and Design of Hybrid Systems, ?
She, Zhikun
Ratschan, Stefan
Providing a Basin of Attraction to a Target Region by Computation of Lyapunov-like Functions
In: 4th IEEE International Conference on Computational Cybernetics, 245-249
She, Zhikun
Xia, Bican
Xiao, Rong
A Semi-Algebraic Approach for the Computation of Lyapunov Functions
In: 2th IASTED International Conference on COMPUTATIONAL INTELLIGENCE, 7-12
Simon, Carlo
Freiheit, Jörn
Olbrich, Sebastian
Using BPEL processes defined by Event-driven Process Chains
In: 5. GI-Workshop "EPK 2006 - Geschäftsprozessmanagement mit Ereignisgesteuerten Prozessketten", 121-135
Sofronie-Stokkermans, VioricaAttachment IconInterpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250
Sofronie-Stokkermans, VioricaSheaves and geometric logic in concurrency
In: Proceedings of the Eighth Workshop on Geometric and Topological Methods in Concurrency (GETCO 2006), ?
Wies, Thomas
Kuncak, Viktor
Lam, Patrick
Podelski, Andreas
Rinard, Martin C.
Attachment IconField Constraint Analysis
In: Verification, Model Checking, and Abstract Interpretation : 7th International Conference, VMCAI 2006, 157-173
5
Hide details for Electronic Proceedings ArticleElectronic Proceedings Article
de Nivelle, Hans
Baumgartner, Peter
Fuchs, Alexander
Tinelli, Cesare
Computing Finite Models by Reduction to Function-Free Clause Logic
In: IJCAR'06 Workshop : Disproving'06: Non-Theorems, Non-Validity, Non-Provability, 82-95
Hillenbrand, Thomas
Topic, Dalibor
Weidenbach, Christoph
Sudokus as Logical Puzzles
In: Proceedings of the Third Workshop on Disproving, 2-12
Jacobs, Swen
Sofronie-Stokkermans, Viorica
Attachment IconApplications of hierarchical reasoning in the verification of complex systems
In: PDPAR'06: Pragmatical Aspects of Decision Procedures in Automated Reasoning, 15-26
Prevosto, VirgileCertified mathematical hierarchies: the FoCal system.
In: Proceedings of the MAP (Mathematics, Algorithms, Proofs) Workshop,
Sofronie-Stokkermans, VioricaLocal reasoning in verification
In: Proceedings of VERIFY'06: Verification Workshop, 128-145
6
Hide details for Journal ArticleJournal Article
Baumgartner, Peter
Fuchs, Alexander
Tinelli, Cesare
Implementing the Model Evolution Calculus
In: International Journal on Artificial Intelligence Tools [15], 21-52
Freiheit, Jörn
Luuk, Marc
Münch, Susanne
Sijanski, Grozdana
Zangl, Fabrice
Lexecute: Visualisation and representation of legal procedures
In: Digital Evidence Journal [3], 17-27
Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Waldmann, Uwe
Modular Proof Systems for Partial Functions with Evans Equality
In: Information and Computation [204], 1453-1492
Hoffmann, Jörg
Brafman, Ronen I.
Conformant planning via heuristic forward search: A new approach
In: Artificial Intelligence [170], 507-541
Jensen, Kurt
Podelski, Andreas
Tools and algorithms for the construction and analysis of systems
In: International Journal on Software Tools for Technology Transfer [8], 177-179
Ratschan, StefanEfficient Solving of Quantified Inequality Constraints over the Real Numbers
In: ACM Transactions on Computational Logic [7], 723-748
2
Hide details for Thesis - Masters thesisThesis - Masters thesis
Dimitrova, RaynaModel Checking with Abstraction Refinement for Well-Structured Systems
Universität des Saarlandes
Schäf, MartinAttachment IconAbstrakte Übergangsrelationen als Mittel zur Verifikation von Programmeigenschaften
Universität des Saarlandes
1
Hide details for Thesis - PhD thesisThesis - PhD thesis
Kazakov, YevgenyAttachment IconSaturation-Based Decision Procedures For Extensions Of The Guarded Fragment
Universität des Saarlandes
1
Hide details for Unpublished/DraftUnpublished/Draft
Malkis, Alexander
Podelski, Andreas
Rybalchenko, Andrey
Attachment IconThread-Modular Verification and Cartesian Abstraction
2
Hide details for MiscellaneousMiscellaneous
Brahm, UweAttachment IconEine integrierte Publikationsverwaltung am Beispiel des Max-Planck-Instituts für Informatik
de Nivelle, Hans
Meng, Jia
Geo 2006j
41
Hide details for 20052005
1
Hide details for Part of a BookPart of a Book
Baumgartner, Peter
Furbach, Ulrich
Living Books, Automated Deduction and other Strange Things
In: Mechanizing Mathematical Reasoning: Techniques, Tools and Applications - Essays in honour of Jörg H. Siekmann, 255-274
22
Hide details for Proceedings ArticleProceedings Article
Baumgartner, Peter
Furbach, Ulrich
Gross-Hardt, Margret
Kleemann, Thomas
Optimizing the Evaluation of XPath Using Description Logics
In: Applications of Declarative Programming and Knowledge Management: 15th International Conference on Applications of Declarative Programming and Knowledge Management, INAP 2004, and 18th Workshop on Logic Programming, WLP 2004, 1-15
Baumgartner, Peter
Tinelli, Cesare
The Model Evolution Calculus with Equality
In: Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 392-408
Charatonik, Witold
Georgieva, Lilia
Maier, Patrick
Bounded Model Checking of Pointer Programs
In: Computer Science Logic; 19th International Workshop, CSL 2005; 14th Annual Conference of the EACSL, 397-412
Cook, Byron
Podelski, Andreas
Rybalchenko, Andrey
Abstraction-refinement for Termination
In: Static analysis : 12th International Symposium, SAS 2005, 87-101
Cuntz, Nicolas
Freiheit, Jörn
Kindler, Ekkart
On the semantics of EPCs: Faster calculation for EPCs with small state spaces
In: EPK 2005 : Geschäftsprozessmanagement mit Ereignisgesteuerten Prozessketten, 7-23
Damm, Werner
Pinto, Guilherme
Ratschan, Stefan
Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems
In: Automated technology for verification and analysis : Third International Symposium, ATVA 2005, 99-113
Daum, Matthias
Maus, Stefan
Schirmer, Norbert
Seghir, Mohammed Nassim
Attachment IconIntegration of a Software Model Checker into Isabelle
In: Logic for Programming, Artificial Intelligence, and Reasoning: 12th International Conference, LPAR 2005, 381-395
de Nivelle, Hans
Piskac, Ruzica
Verification of an Off-Line Checker for Priority Queues
In: Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 210-219
Freiheit, Jörn
Münch, Susanne
Schöttle, Hendrik
Sijanski, Grozdana
Zangl, Fabrice
Attachment IconEnhanced Workflow Models as a Tool for Judicial Practitioners
In: On the move to meaningful internet systems 2005: OTM 2005 Workshops : OTM Confederated International Workshops and Posters, AWeSOMe, CAMS, GADA, MIOS+INTEROP, ORM, PhDS, SeBGIS, SWWS, and WOSE 2005, 26-27
Georgieva, Lilia
Maier, Patrick
Description Logics for Shape Analysis
In: Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 321-330
Hoenicke, Jochen
Maier, Patrick
Model-Checking of Specifications Integrating Processes, Data and Time
In: FM 2005: Formal Methods; International Symposium of Formal Methods Europe, 465-480
Hoffmann, Jörg
Brafman, Ronen
Contingent Planning via Heuristic Forward Search with Implicit Belief States
In: 15th International Conference on Automated Planning and Scheduling, 71-80
Jacobs, Swen
Waldmann, Uwe
Attachment IconComparing Instance Generation Methods for Automated Reasoning
In: Automated reasoning with analytic tableaux and related methods : International Conference, TABLEAUX 2005, 153-168
Pnueli, Amir
Podelski, Andreas
Rybalchenko, Andrey
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems
In: Tools and Algorithms for the Construction and Analysis of Systems: 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, 124-139
Podelski, Andreas
Rybalchenko, Andrey
Transition predicate abstraction and fair termination
In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, 124-139
Podelski, Andreas
Schaefer, Ina
Wagner, Silke
Attachment IconSummaries for While Programs with Recursion
In: Programming Languages and Systems: 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, 94-107
Podelski, Andreas
Wies, Thomas
Boolean Heaps
In: Static analysis : 12th International Symposium, SAS 2005, 268-283
Prevosto, Virgile
Boulmé, Sylvain
Proof Contexts with Late Binding
In: Typed Lambda Calculi and Applications: 7th International Conference, TLCA 2005, 325-339
Ratschan, StefanSolving Undecidable Problems in the Theory of Real Numbers and Hybrid Systems
In: Algorithmic Algebra and Logic; Conference in Honor of the 60th Birthday of Volker Weispfenning, 213-216
Ratschan, Stefan
She, Zhikun
Safety Verification of Hybrid Systems by Constraint Propagation Based Abstraction Refinement
In: Hybrid Systems: Computation and Control: 8th International Workshop, HSCC 2005, 573-589
Sofronie-Stokkermans, VioricaAttachment IconHierarchic reasoning in local theory extensions
In: Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 219-234
Yuan, Cong
Billington, Jonathan
Freiheit, Jörn
Attachment IconAn Abstract Model of Routing in Mobile Ad Hoc Networks
In: Sixth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, 137-156
1
Hide details for PosterPoster
Hoffmann, JörgA Covering Problem for Hypercubes
In: Proceedings of the 19th International Joint Conference on Artificial Intelligence, 579-580
11
Hide details for Journal ArticleJournal Article
Baumgartner, Peter
Furbach, Ulrich
Yahya, Adnan
Automated Reasoning, Knowledge Representation and Management
In: KI - Künstliche Intelligenz [1], 5-11
Blanchet, Bruno
Podelski, Andreas
Verification of Cryptographic Protocols: Tagging Enforces Termination
In: Theoretical Computer Science [333], 67-90
de Nivelle, HansTranslation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
In: Information and Computation [199], 24-54
de Nivelle, Hans
Demri, Stéphane
Deciding Regular Grammar Logics with Converse through First-Order Logic
In: Journal of Logic, Language and Information [14], 289-329
Delahaye, David
Jaume, Mathieu
Prevosto, Virgile
Coq, un outil pour l'enseignement
In: Technique et Science Informatiques [24], 1139-1160
Ganzinger, Harald
Stuber, Jürgen
Superposition with equivalence reasoning and delayed clause normal form transformation
In: Information and Computation [199], 3-23
Goncharov, Sergey
Harizanov, Valentina
Knight, Julia F.
Morozov, Andrey
Romina, Anya
On automorphic tuples of elements in computable models
In: Siberian Mathematical Journal [46], 405-412
Hoffmann, JörgIn Defense of PDDL Axioms
In: Artificial Intelligence [168], 38-69
Hoffmann, JörgThe Deterministic Part of IPC-4: An Overview
In: Journal of Artificial Intelligence Research [24], 519 - 579
Hoffmann, JörgWhere Ignoring Delete Lists Works: Local Search Topology in Planning Benchmarks
In: Journal of Artificial Intelligence Research [24], 685-758
Korovin, Konstantin
Voronkov, Andrei
Knuth-Bendix constraint solving is NP-complete
In: ACM Transactions on Computational Logic [6], 361-388
2
Hide details for Thesis - Masters thesisThesis - Masters thesis
Piskac, RuzicaFormal Correctness of Result Checking for Priority Queues
Universität des Saarlandes
Suchanek, Fabian M.Ontological Reasoning for Natural Language Understanding
Universität des Saarlandes
1
Hide details for Thesis - PhD thesisThesis - PhD thesis
Backes, WernerProgrammanalyse des XRTL Zwischencodes
Universität des Saarlandes
1
Hide details for Thesis - otherThesis - other
Hagemann, WillemFormalisierung der Arithmetik
Universität Göttingen
2
Hide details for Unpublished/DraftUnpublished/Draft
Baumgartner, Peter
Suchanek, Fabian
Attachment IconModel-Generation Theorem Proving for First-Order Logic Ontologies
Podelski, Andreas
Rybalchenko, Andrey
Cook, Byron
Counterexample-Guided Abstraction Refinement for Termination
37
Hide details for 20042004
1
Hide details for ProceedingsProceedings
Jensen, Podelski (ed.)Tools and algorithms for the construction and analysis of systems : 10th International Conference, TACAS 2004 ; held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004
19
Hide details for Proceedings ArticleProceedings Article
Baumgartner, Peter
Burchardt, Aljoscha
Logic Programming Infrastructure for Inferences on FrameNet
In: Logics in artificial intelligence : 9th European Conference, JELIA 2004, 591-603
Baumgartner, Peter
Fuchs, Alexander
Tinelli, Cesare
Darwin: A Theorem Prover for the Model Evolution Calculus
In: Proceedings of the 1st Workshop on Empirically Successful First Order Reasoning (ESFOR'04), 1-24
Baumgartner, Peter
Furbach, Ulrich
Gross-Hardt, Margret
Kleemann, Thomas
Model Based Deduction for Database Schema Reasoning
In: KI 2004: Advances in Artificial Intelligence: 27th Annual German Conference on AI, KI 2004, 168-182
Baumgartner, Peter
Mediratta, Anupam
Improving Stable Models Based Planning by Bidirectional Search
In: Proceedings of the 5th International Conference on Knowledge Based Computer Systems (KBCS 2004), 404-413
Brafman, Ronen
Hoffmann, Jörg
Conformant Planning via Heuristic Forward Search: A New Approach
In: Proceedings of the Fourteenth International Conference on Automated Planning and Scheduling (ICAPS 2004), 355-364
Dubois, Catherine
Jaume, Mathieu
Pons, Olivier
Prevosto, Virgile
L'atelier FOCAL
In: Actes du 6ème Atelier sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2004), 321-324
Ganzinger, Harald
Hagen, George
Nieuwenhuis, Robert
Oliveras, Albert
Tinelli, Cesare
DPLL(T): Fast Decision Procedures
In: Computer aided verification : 16th International Conference, CAV 2004, 175-188
Ganzinger, Harald
Korovin, Konstantin
Integration of equational reasoning into instantiation-based theorem proving
In: Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL, 71-84
Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Waldmann, Uwe
Modular Proof Systems for Partial Functions with Weak Equality
In: Automated reasoning : Second International Joint Conference, IJCAR 2004, 168-182
Goranko, Valentin
Hustadt, Ullrich
Schmidt, Renate A.
Vakarelov, Dimiter
SCAN is complete for all Sahlqvist formulae
In: Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, 149-162
Kazakov, YevgenyAttachment IconA Polynomial Translation from the Two-Variable Guarded Fragment with Number Restrictions to the Guarded Fragment
In: Logics in artificial intelligence : 9th European Conference, JELIA 2004, 372-384
Kazakov, Yevgeny
de Nivelle, Hans
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards
In: Automated reasoning : Second International Joint Conference, IJCAR 2004, 122-136
Maier, PatrickIntuitionistic LTL and a New Characterization of Safety and Liveness
In: Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL, 295-309
Podelski, Andreas
Rybalchenko, Andrey
A Complete Method for the Synthesis of Linear Ranking Functions
In: Verification, model checking, and abstract interpretation : 5th International Conference, VMCAI 2004, 239-251
Podelski, Andreas
Rybalchenko, Andrey
Transition Invariants
In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, LICS 2004, 32-41
Ratschan, Stefan
Vehi, Josep
Attachment IconRobust Pole Clustering of Parametric Uncertain Systems Using Interval Methods
In: Robust control design 2003 : (ROCOND 2003) ; a proceedings volume from the 4th IFAC symposium, 323-328
Schmidt, Renate A.
Orłowska, Ewa
Hustadt, Ullrich
Two Proof Systems for Peirce Algebras
In: Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, 238-251
Sofronie-Stokkermans, VioricaResolution-based decision procedures for the positive theory of some finitely generated varieties of algebras
In: Proceedings of the 34th International Symposium on Multiple-Valued Logic (ISMVL-2004), 32-37
Trueg, Sebastian
Hoffmann, Jörg
Nebel, Bernhard
Applying Automatic Planning Systems to Airport Ground Traffic Control -- A Feasibility Study
In: KI 2004: Advances in Artificial Intelligence: 27th Annual German Conference on AI, KI 2004, 183-197
1
Hide details for Electronic Proceedings ArticleElectronic Proceedings Article
Hillenbrand, ThomasAttachment IconA Superposition View on Nelson-Oppen
In: Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning, 16-20
9
Hide details for Journal ArticleJournal Article
Baumgartner, Peter
Furbach, Ulrich
Gross-Hardt, Margret
Sinner, Alex
Living Book -- Deduction, Slicing, and Interaction
In: Journal of Automated Reasoning [32], 259-286
Baumgartner, Peter
Grabowski, Barbara
Oevel, Walter
Melis, Erica
In2Math - Interaktive Mathematik- und Informatikgrundausbildung
In: Softwaretechnik-Trends [24], 36-45
Ganzinger, Harald
Nieuwenhuis, Robert
Nivela, Pilar
Attachment IconFast Term Indexing with Coded Context Trees
In: Journal of Automated Reasoning [32], 103-120
Hoffmann, Jörg
Porteous, Julie
Sebastia, Laura
Ordered Landmarks in Planning
In: Journal of Artificial Intelligence Research [22], 215-278
Jaulin, Luc
Ratschan, Stefan
Hardouin, Laurent
Set Computation for Nonlinear Control
In: Reliable Computing [10], 1-26
Podelski, AndreasIntroduction to the Special Issue on Verification and Computational Logic
In: Theory and Practice of Logic Programming (TPLP) [4], 541-751
Ratschan, StefanConvergent Approximate Solving of First-order Constraints by Approximate Quantifiers
In: ACM Transactions on Computational Logic [5], 264-281
Schmidt, Renate A.
Tishkovsky, Dmitry
Multi-Agent Dynamic Logics with Informational Test
In: Annals of Mathematics and Artificial Intelligence [42], 5-36
Schmidt, Renate A.
Tishkovsky, Dmitry
Hustadt, Ullrich
Interaction between Knowledge, Action and Commitment within Agent Dynamic Logic
In: Studia Logica [78], 381-415
3
Hide details for ReportReport
de Nivelle, Hans
Kazakov, Yevgeny
Attachment IconResolution Decision Procedures for the Guarded Fragment with
Transitive Guards
Maier, PatrickAttachment IconIntuitionistic LTL and a New Characterization of Safety and Liveness
Podelski, Andreas
Schaefer, Ina
Wagner, Silke
Attachment IconSummaries for While Programs with Recursion
2
Hide details for Thesis - Masters thesisThesis - Masters thesis
Jacobs, SwenAttachment IconInstance Generation Methods for Automated Reasoning
Universität des Saarlandes
Wies, ThomasAttachment IconSymbolic Shape Analysis
Universität des Saarlandes
1
Hide details for Thesis - Habilitation thesisThesis - Habilitation thesis
Sofronie-Stokkermans, VioricaAlgebraic and logical methods in automated theorem proving and in the study of concurrency
Universität des Saarlandes
1
Hide details for Unpublished/DraftUnpublished/Draft
Lee, Chin SoonSize-change Termination Analyzer
36
Hide details for 20032003
1
Hide details for BookBook
Hoffmann, JörgUtilizing Problem Structure in Planning: A Local Search Approach
2
Hide details for Part of a BookPart of a Book
Schmidt, Renate A.
Tishkovsky, Dmitry
Combining Dynamic Logic and Doxastic Modal Logics
In: Advances in Modal Logic, 371-391
Sofronie-Stokkermans, VioricaAttachment IconRepresentation Theorems and the Semantics of Non-classical Logics, and Applications to Automated Theorem Proving
In: Beyond Two: Theory and Applications of Multiple Valued Logic, 59-100
21
Hide details for Proceedings ArticleProceedings Article
Blanchet, Bruno
Podelski, Andreas
Verification of Cryptographic Protocols: Tagging Enforces Termination
In: Foundations of software science and computation structures : 6th International Conference, FOSSACS 2003, 136-152
de Nivelle, HansImplementing the clausal normal form transformation with proof generation
In: Fourth Workshop on the Implementation of Logics, 69-83
de Nivelle, HansTranslation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 365-379
de Nivelle, Hans
Demri, Stéphane
Deciding Modal Logics through Relational Translations into GF2
In: Proceedings of the 3rd Methods for Modalities Workshop, 15-30
Gaillourdet, Jean-Marie
Hillenbrand, Thomas
Löchner, Bernd
Spies, Hendrik
Attachment IconThe New WALDMEISTER Loop at Work
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 317-321
Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe
Attachment IconSuperposition modulo a Shostak Theory
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 182-196
Ganzinger, Harald
Korovin, Konstantin
Attachment IconNew Directions in Instantiation-Based Theorem Proving
In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), 55-64
Ganzinger, Harald
Stuber, Jürgen
Attachment IconSuperposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 335-349
Hoffmann, Jörg
Geffner, Hector
Branching Matters: Alternative Branching in Graphplan
In: 13th International Conference on Automated Planning and Scheduling (ICAPS-13), 22-31
Jaeger, ManfredAttachment IconA Representation Theorem and Applications
In: Symbolic and Quantitative Approaches to Reasoning with Uncertainty :
7th European Conference, ECSQARU 2003, 50-61
Jaeger, ManfredProbabilistic Classifiers and the Concepts they Recognize
In: Proceedings of the Twentieth International Conference on Machine Learning (ICML-03), 266-273
Kazakov, Yevgeny
de Nivelle, Hans
Attachment IconSubsumption of Concepts in $FL_0$ for (Cyclic) Terminologies with Respect to Descriptive Semantics is PSPACE-complete
In: 2003 International Workshop on Description Logics (DL-03), 56-64
Korovin, Konstantin
Voronkov, Andrei
Attachment IconAC-compatible Knuth-Bendix Order
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 47-59
Korovin, Konstantin
Voronkov, Andrei
Attachment IconOrienting Equalities with the Knuth-Bendix Order
In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), 75-84
Letz, Reinhold
Stenz, Gernot
Universal variables in disconnection tableaux
In: Automated reasoning with analytical tableaux and related methods : International Conference, TABLEAUX 2003, 117-133
Maier, PatrickCompositional Circular Assume-Guarantee Rules Cannot Be Sound and Complete
In: Foundations of software science and computation structures : 6th International Conference, FOSSACS 2003, 343-357
Podelski, AndreasSoftware Model Checking with Abstraction Refinement
In: Verification, model checking, and abstract interpretation : 4th International Conference, VMCAI 2003, 1-13
Ratschan, StefanSolving Existentially Quantified Constraints with One Equality and Arbitrarily Many Inequalities
In: Principles and practice on constraint programming - CP 2003 : 9th International Conference, CP 2003, 615-633
Schmidt, Renate A.
Hustadt, Ullrich
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 412-426
Sofronie-Stokkermans, VioricaAttachment IconAutomated theorem proving by resolution in non-classical logics
In: Fourth International Conference Journees de l'Informatique Messine: Knowledge Discovery and Discrete Mathematics (JIM-03), 151-167
Thiebaux, Sylvie
Hoffmann, Jörg
Nebel, Bernhard
In Defense of PDDL Axioms
In: 18th International Joint Conference on Artificial Intelligence, 961-966
1
Hide details for Electronic Proceedings ArticleElectronic Proceedings Article
Hillenbrand, ThomasAttachment IconCitius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER
In: Proceedings of the 4th International Workshop on First Order Theorem Proving, FTP'03, 1-13
7
Hide details for Journal ArticleJournal Article
Avenhaus, Jürgen
Hillenbrand, Thomas
Löchner, Bernd
Attachment IconOn Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233
Charatonik, Witold
Dal Zilio, Silvano
Gordon, Andrew Donald
Mukhopadhyay, Supratik
Talbot, Jean-Marc
Model checking mobile ambients
In: Theoretical Computer Science [308], 277-331
de Nivelle, Hans
de Rijke, Maarten
Deciding the Guarded Fragments by Resolution
In: Journal of Symbolic Computation [35], 21-58
Hoffmann, JörgThe Metric-FF Planning System: Translating ``Ignoring Delete Lists'' To Numeric State Variables
In: Journal of Artificial Intelligence Research [20], 51
Korovin, Konstantin
Voronkov, Andrei
Orienting rewrite rules with the Knuth-Bendix order
In: Information and Computation [183], 165-186
Podelski, Andreas
Ball, Tom
Rajamani, Sriram K.
Boolean and Cartesian Abstraction for Model Checking C Programs
In: International Journal on Software Tools for Technology Transfer (STTT) [5], 1-15
Sofronie-Stokkermans, VioricaAttachment IconResolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
In: Journal of Symbolic Computation [36], 891-924
1
Hide details for ReportReport
de Nivelle, Hans
Demri, Stéphane
Deciding regular grammar logics with converse through first-order logic
2
Hide details for Thesis - PhD thesisThesis - PhD thesis
Korovin, KonstantinKnuth-Bendix orders in automated deduction and term rewriting
University of Manchester
Maier, PatrickAttachment IconA Lattice-Theoretic Framework For Circular Assume-Guarantee Reasoning
Universität des Saarlandes
1
Hide details for Unpublished/DraftUnpublished/Draft
Schmidt, Renate A.
Tishkovsky, Dmitry
Multi-Agent Logic of Dynamic Belief and Knowledge
39
Hide details for 20022002
1
Hide details for Part of a BookPart of a Book
Basin, David A.
Matthews, Sean
Logical Frameworks
In: Handbook of Philosophical Logic, 89-164
23
Hide details for Proceedings ArticleProceedings Article
Charatonik, Witold
Amadio, Roberto
On Name Generation and Set-Based Analysis in the Dolev-Yao Model
In: CONCUR 2002 - Concurrency Theory. 13th International Conference, 499-514
Charatonik, Witold
Gordon, Andrew Donald
Talbot, Jean-Marc
Finite-Control Mobile Ambients
In: Programming languages and systems: 11th European Symposium on Programming, ESOP 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, 295-313
Charatonik, Witold
Mukhopadhyay, Supratik
Podelski, Andreas
Compositional Termination Analysis of Symbolic Forward Analysis
In: Verification, Model Checking, and Abstract Interpretation. Third International Workshop, VMCAI 2002, 109-125
Charatonik, Witold
Mukhopadhyay, Supratik
Podelski, Andreas
Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP
In: Logic Programming. 18th International Conference, ICLP 2002, 115-129
Charatonik, Witold
Talbot, Jean-Marc
Atomic Set Constraints with Projection
In: Rewriting Techniques and Applications. 13th International Conference, RTA 2002, 311-325
de Nivelle, HansExtraction of Proofs from the Clausal Normal Form Transformation
In: Computer Science Logic : 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, 584-598
de Raedt, Luc
Jaeger, Manfred
Lee, Sau Dan
Mannila, Heikki
Attachment IconA Theory of Inductive Query Answering
In: Proceedings of the 2002 IEEE International Conference on Data Mining (ICDM'02), 123-130
Eisenbrand, Friedrich
Rinaldi, Giovanni
Ventura, Paolo
0/1 Optimization and 0/1 Primal Separation are Equivalent
In: Proceedings of the 13th Annual ACM SIAM Symposium on Discrete Algorithms, 920-926
Ganzinger, HaraldAttachment IconShostak Light
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 332-346
Ganzinger, Harald
McAllester, David
Attachment IconLogical Algorithms
In: Logic Programming. 18th International Conference, ICLP 2002, 209-223
Georgieva, Lilia
Hustadt, Ullrich
Schmidt, Renate A.
A New Clausal Class Decidable by Hyperresolution
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 260-274
Georgieva, Lilia
Hustadt, Ullrich
Schmidt, Renate A.
On the Relationship Between Decidable Fragments, Non-Classical Logics, and Description Logics
In: Proceedings of the International Workshop on Description Logics (DL'2002), 25-36
Hillenbrand, Thomas
Löchner, Bernd
Attachment IconThe Next WALDMEISTER Loop
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 486-500
Hillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor
Attachment IconIs Logic Effective for Analyzing C Programs?
In: Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, 27-30
Jaeger, ManfredAttachment IconProbababilistic Decision Graphs - Combining Verification and AI Techniques for Probabilistic Inference
In: Proceedings of the First European Workshop on Probabilistic Graphical Models, 81-88
Kazakov, YevgenyAttachment IconRecursive resolution for modal logic
In: Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, 11-15
Maier, PatrickA Framework for Circular Assume-Guarantee Rules
In: Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, 55-58
Mukhopadhyay, Supratik
Podelski, Andreas
An Algebraic Framework for Abstract Model Checking
In: Abstraction, reformulation, and approximation : 5th International Symposium, SARA 2002, 152-169
Podelski, Andreas
Ball, Tom
Rajamani, Sriram K.
Relative Completeness of Abstraction Refinement for Software Model Checking
In: Tools and algorithms for the construction and analysis of systems : 8th International Conference, TACAS 2002, 158-172
Schmidt, Renate A.
Tishkovsky, Dmitry
Multi-Agent Logic of Dynamic Belief and Knowledge
In: Proceedings of the 8th European Conference on Logics in Artificial Intelligence (JELIA), 38-49
Sofronie-Stokkermans, VioricaAttachment IconOn uniform word problems involving bridging operators on distributive lattices
In: Automated Reasoning with Analytic and Related Methods : International Conference, TABLEAUX 2002, 235-250
Waldmann, UweA New Input Technique for Accented Letters in Alphabetical Scripts
In: Proceedings of the 20th International Unicode Conference, C12
Weidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor
Attachment IconSPASS Version 2.0
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 275-279
9
Hide details for Journal ArticleJournal Article
Bezem, Marc
Hendriks, Dimitri
de Nivelle, Hans
Automated Proof Construction in Type Theory using Resolution
In: Journal of Automated Reasoning [29], 253-275
Charatonik, Witold
Podelski, Andreas
Set Constraints with Intersection
In: Information and Computation [179], 213-229
Lang, Jérôme
van der Torre, Leendert W. N.
Weydert, Emil
Utilitarian Desires
In: Autonomous Agents and Multi-Agent Systems [5], 329-363
Löchner, Bernd
Hillenbrand, Thomas
Attachment IconA Phytography of WALDMEISTER
In: AI Communications [15], 127-133
Vorobyov, SergeiThe undecidability of the first-order theories of one step rewriting in linear canonical systems
In: Information and Computation [175], 182-213
Vorobyov, Sergei$\forall\exists^5$-equational theory of context unification is undecidable
In: Theoretical Computer Science [275], 463-479
Waldmann, UweCancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II)
In: Journal of Symbolic Computation [33], 831-861
Waldmann, UweCancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I)
In: Journal of Symbolic Computation [33], 777-829
Xia, Bican
Yang, Lu
An Algorithm for Isolating the Real Solutions of Semi-algebraic Systems
In: Journal of Symbolic Computation [34], 461-477
1
Hide details for Electronic Journal ArticleElectronic Journal Article
Jaeger, ManfredAttachment IconRelational Bayesian Networks: a Survey
In: Electronic Transactions on Artificial Intelligence [6],
1
Hide details for ReportReport
Georgieva, Lilia
Hustadt, Ullrich
Schmidt, Renate A.
A New Clausal Class Decidable by Hyperresolution
1
Hide details for Thesis - Masters thesisThesis - Masters thesis
Rybalchenko, AndreyAttachment IconA Model Checker based on Abstraction Refinement
Universität des Saarlandes
2
Hide details for Thesis - Habilitation thesisThesis - Habilitation thesis
Charatonik, WitoldDirektionale Typen in der Logischen Programmierung
Universität des Saarlandes
Jaeger, ManfredProbabilistic Decision Graphs
Universität des Saarlandes
1
Hide details for Unpublished/DraftUnpublished/Draft
Schmidt, Renate A.
Tishkovsky, Dmitry
Hustadt, Ullrich
Interaction between Knowledge, Action and Commitment within Agent Dynamic Logic
58
Hide details for 20012001
7
Hide details for Part of a BookPart of a Book
Bachmair, Leo
Ganzinger, Harald
Attachment IconResolution Theorem Proving
In: Handbook of Automated Reasoning, 19-99
Bockmayr, Alexander
Weispfenning, V.
Solving numerical constraints
In: Handbook of Automated Reasoning, 751-842
Fermüller, Christian G.
Leitsch, Alexander
Hustadt, Ullrich
Tammet, Tanel
Resolution Decision Procedures
In: Handbook of Automated Reasoning, 1793-1849
Ganzinger, Harald
Hustadt, Ullrich
Meyer, Christoph
Schmidt, Renate A.
Attachment IconA Resolution-Based Decision Procedure for Extensions of K4
In: Advances in Modal Logic, Volume 2, 225-246
Nonnengart, Andreas
Ohlbach, Hans Jürgen
Gabbay, Dov M.
Encoding two-valued non-classical logics in classic logic
In: Handbook of Automated Reasoning, 1403-1486
Nonnengart, Andreas
Weidenbach, Christoph
Computing small clause normal forms
In: Handbook of Automated Reasoning, 335-367
Weidenbach, ChristophCombining Superposition, Sorts and Splitting
In: Handbook of Automated Reasoning, 1965-2013
1
Hide details for ProceedingsProceedings
de Nivelle, Schulz (ed.)Proceedings of the 2nd International Workshop on the Implementation of Logics
28
Hide details for Proceedings ArticleProceedings Article
Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph
Attachment IconFirst-Order Atom Definitions Extended
In: Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001), 309-319
Argon, Pablo
Delzanno, Giorgio
Mukhopadhyay, Supratik
Podelski, Andreas
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
Backes, Werner
Wetzel, Susanne
Lattice Basis Reduction with Dynamic Approximation
In: Proceedings of the 4th Workshop On Algorithm Engineering (WAE-2000), 63-73
Ball, Thomas
Podelski, Andreas
Rajamani, Sriram K.
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
Charatonik, Witold
Dal Zilio, Silvano
Gordon, Andrew Donald
Mukhopadhyay, Supratik
Talbot, Jean-Marc
The Complexity of Model Checking Mobile Ambients
In: Foundations of Software Science and Computation Structures. Proceedings of the 4th International Conference (FOSSACS-01). Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS-01), 152-167
Charatonik, Witold
Talbot, Jean-Marc
The Decidability of Model Checking Mobile Ambients
In: Computer science logic (CSL-01) : 15th International Workshop, CSL 2001, Annual Conference of the EACSL, 339-354
de Nivelle, HansSplitting through New Proposition Symbols
In: Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001), 172-185
de Nivelle, Hans
Pratt-Hartmann, Ian
A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 211-225
Eisenbrand, Friedrich
Rote, Günter
Fast 2-variable integer programming
In: Proceedings of the 8th Conference on Integer and Combinatorial Optimization (IPCO-01), 78-89
Eisenbrand, Friedrich
Rote, Günter
Fast reduction of ternary quadratic forms
In: Proceedings of the 1st Conference on Lattices and Cryptography (CaLC-01), 99-111
Ganzinger, HaraldBottom-Up Deduction with Deletion and Priorities
In: Programs as Data Objects (PADO-01) : Second Symposium PADO 2001, 276-277
Ganzinger, HaraldAttachment IconRelating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems
In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS-01), 81-90
Ganzinger, Harald
McAllester, David
Attachment IconA new meta-complexity theorem for bottom-up logic programs
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 514-528
Ganzinger, Harald
Nieuwenhuis, Robert
Attachment IconConstraints and Theorem Proving
In: Contraints in Computational Logics, International Summer School (CCL-99), 159-201
Ganzinger, Harald
Nieuwenhuis, Robert
Nivela, Pilar
Attachment IconContext trees
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 242-256
Hillenbrand, Thomas
Löchner, Bernd
Attachment IconThe Next WALDMEISTER Loop (Extended Abstract)
In: Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001, 13-21
Jaeger, ManfredAttachment IconConstraints as Data: a New Perspective on Inferring Probabilities
In: Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI-01), 755-760
Lang, Jérôme
van der Torre, Leendert W. N.
Weydert, Emil
Two Kinds of Conflicts between Desires (and how to resolve them)
In: Proceedings of the AAAI Symposium on Game and Decision Theoretic Agents, 54-59
Maier, PatrickA Set-Theoretic Framework for Assume-Guarantee Reasoning
In: Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP-2001), 821-834
Makinson, David
van der Torre, Leendert W. N.
Input-output logics
In: Proceedings of the 5th International Workshop on Deontic Logic in Computer Science (Deon-00),, 29
Mukhopadhyay, Supratik
Podelski, Andreas
Accurate Widenings and Boundedness Properties of Timed Systems
In: Perspectives of System Informatics: 4th International Andrei Ershov Memorial Conference, 79-94
Mukhopadhyay, Supratik
Podelski, Andreas
Attachment IconConstraint Database Models Characterizing Timed Bisimilarity
In: Proceedings of the 3rd International Symposium on Practical Aspects of Declarative Languages, 245-258
Nielson, Flemming
Seidl, Helmut
Control-Flow Analysis in Cubic Time
In: Proceedings of the 10th European Symposium on Programming (ESOP-01) held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS-01), 252-268
Nieuwenhuis, Robert
Hillenbrand, Thomas
Riazanov, Alexandre
Voronkov, Andrei
Attachment IconOn the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271
Sofronie-Stokkermans, VioricaRepresentation theorems and the semantics of (semi)lattice-based logics
In: Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logics, 125-134
Waldmann, UweSuperposition and Chaining for Totally Ordered Divisible Abelian Groups (Extended Abstract)
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 226-241
Weydert, EmilRankings we prefer: a minimal construction semantics for default reasoning
In: Proceedings of the 6th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU-01), 616-627
Weydert, EmilRankings we prefer: a rational minimal construction semantics for default reasoning
In: Proceedings of the 5th Dutch-German Workshop on Nonmonotonic Reasoning Techniques and their Applications (DGNMR-01), 1-12
14
Hide details for Journal ArticleJournal Article
Areces, Carlos
de Rijke, Maarten
de Nivelle, Hans
Resolution in modal, description and hybrid logic
In: Journal of Logic and Computation [11], 717-736
Ayari, Abdelwaheb
Basin, David A.
A Higher-order Interpretation of Deductive Tableau
In: Journal of Symbolic Computation [31], 487-520
Basin, David A.
Ganzinger, Harald
Attachment IconAutomated Complexity Analysis Based on Ordered Resolution
In: Journal of the ACM [48], 70-109
Bockmayr, Alexander
Eisenbrand, Friedrich
Cutting planes and the elementary closure in fixed dimension
In: Mathematics of Operations Research [26], 304-312
Booth, RichardThe lexicographic closure as a revision process
In: Journal of Applied Non-Classical Logics [11], 35-58
de Nivelle, Hans
Blackburn, Patrick
Bos, Johan
Kohlhase, Michael
Inference and Computational Semantics
In: Studies in Linguistics and Philosophy, Computing Meaning [77], 11-28
Delzanno, Giorgio
Podelski, Andreas
Constraint-based Deductive Model Checking
In: International Journal on Software Tools for Technology Transfer (STTT) [3], 250-270
Eisenbrand, FriedrichShort vectors of planar integral lattices via continued fractions
In: Information Processing Letters [79], 121-126
Ganzinger, HaraldEfficient deductive methods for program analysis
In: ACM SIGPLAN Notices [36], 102-103
Jaeger, ManfredAttachment IconAutomatic Derivation of Probabilistic Inference Rules
In: International Journal of Approximate Reasoning [28], 1-22
Jaeger, ManfredAttachment IconComplex Probabilistic Modeling with Recursive Relational Bayesian Networks
In: Annals of Mathematics and Artificial Intelligence [32], 179-220
Sofronie-Stokkermans, VioricaAttachment IconAutomated Theorem Proving by Resolution for Finitely-Valued Logics Based on Distributive Lattices with Operators
In: Multiple-Valued Logic - An International Journal [6], 289-344
van der Torre, Leendert W. N.
Weydert, Emil
Parameters for Utilitarian Desires in a Qualitative Decision Theory
In: Applied Artificial Intelligence [14], 285-301
Weydert, EmilDefaults, Logic and Probability - A theoretical perspective
In: KI - Künstliche Intelligenz [4/01], 44-49
1
Hide details for ReportReport
Charatonik, Witold
Dal Zilio, Silvano
Gordon, Andrew Donald
Mukhopadhyay, Supratik
Talbot, Jean-Marc
The Complexity of Model Checking Mobile Ambients
2
Hide details for Thesis - Masters thesisThesis - Masters thesis
Grenner, IngoDie Erzeugung von Schnittebenen mit maximalem Verletzungsgrad und deren Einsatz im Branch-and-Cut Verfahren
Universität des Saarlandes
Jung, GeorgAttachment IconEin Frontend für die Anwendung von Model Checking auf die Analyse von Array Bounds für C Programme
Universität des Saarlandes
3
Hide details for Thesis - PhD thesisThesis - PhD thesis
Gamkrelidze, AlexanderAttachment IconEinige Optimierungsmethoden hierarchischer Schaltkreise
Universität des Saarlandes
Hopf, JörnPhotomaskenlayout für eine 3D-Grauton-Lithographie als kombinatorisches Optimierungsproblem
Universität des Saarlandes
Mukhopadhyay, SupratikAttachment IconA Uniform Constraint-based Framework for the Verification of Infinite State Systems
Universität des Saarlandes
2
Hide details for Unpublished/DraftUnpublished/Draft
Nonnengart, AndreasStrong Skolemization
Nonnengart, Andreas
Ohlbach, Hans Jürgen
Szalas, Andrzej
Quantifier Elimination for Second-Order Predicate Logic
48
Hide details for 20002000
4
Hide details for Part of a BookPart of a Book
Iturrioz, Luisa
Sofronie-Stokkermans, Viorica
SHn-algebras (Symmetric Heyting algebras of order n)
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-11
Schmidt, Renate A.Relational Grammars for Knowledge Representation
In: Variable-Free Semantics, 162-180
Sofronie-Stokkermans, VioricaSome properties of Kleene algebras
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-7
Wu, JinzhaoFirst-Order Polynomial based Theorem Proving
In: Mathematics Mechanizations and Applications, 273-294
1
Hide details for ProceedingsProceedings
Furbach, Ganzinger, Hasegawa, Kapur (ed.)Deduction
19
Hide details for Proceedings ArticleProceedings Article
Backes, Werner
Wetzel, Susanne
New Results on Lattice Basis Reduction in Practice
In: Proceedings of the 4th International Algorithmic Number Theory Symposium (ANTS-IV), 135-152
Charatonik, WitoldDirectional Type Checking for Logic Programs: Beyond Discriminative Types
In: Proceedings of the 8th European Symposium on Programming (ESOP-00), 72-87
Charatonik, Witold
Podelski, Andreas
Talbot, Jean-Marc
Paths vs. Trees in Set-based Program Analysis
In: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL-00), 330-337
de Nivelle, HansAn Overview of Resolution Decision Procedures
In: Formalizing the Dynamics of Information, 115-130
de Nivelle, Hans
Bezem, Marc
Hendriks, Dimitri
Automated Proof Construction in Type Theory Using Resolution
In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), 148-163
Delzanno, Giorgio
Raskin, Jean-François
Symbolic Representation of Upward-Closed Sets
In: Proceedings of the 6th Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS-00); Held as Part of the European Joint Conferences on the Theory and Practice of Software (ETAPS-00), 426-440
Eisenbrand, Friedrich
Bockmayr, Alexander
Combining logic and optimization in cutting plane theory
In: Proceedings of the Workshop on Frontiers of Combining Systems (FROCOS-2000), 1-17
Esparza, Javier
Podelski, Andreas
Efficient Algorithms for Pre$^\star$ and Post$^\star$ on Interprocedural Parallel Flow Graphs
In: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL-00), 1-11
Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Attachment IconChaining Techniques for Automated Theorem Proving in Many-Valued Logics
In: Proceedings of the 30th IEEE International Symposium on Multiple-Valued Logic (ISMVL-00), 337-344
Göbel, Manfred
Maier, Patrick
Three Remarks on Comprehensive Gröbner and SAGBI Bases
In: Proceedings of the 3rd Workshop on Computer Algebra in Scientific Computing (CASC-2000), 191-202
Mukhopadhyay, Supratik
Podelski, Andreas
Model Checking for Timed Logic Processes
In: Proceedings of the 1st International Conference on Computational Logic, 598-612
Podelski, AndreasModel Checking as Constraint Solving
In: Proceedings of the 7th International Symposium on Static Analysis (SAS-00), 221-237
Sofronie-Stokkermans, VioricaAttachment IconOn unification for bounded distributive lattices
In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), 465-481
Sofronie-Stokkermans, VioricaAttachment IconResolution-based theorem proving for SHn-logics
In: Automated Deduction in Classical and Non-Classical Logic (Selected Papers of FTP'98), 268-282
Stuber, JürgenDeriving Theory Superposition Calculi from Convergent Term Rewriting Systems
In: Proceedings of the 11th International Conference Rewriting Techniques and Applications (RTA-00), 229-245
Talbot, Jean-MarcOn the Alternation-free Horn mu-calculus
In: Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR-2000), 418-435
Weydert, EmilHow to revise ranked probabilities
In: Proceedings of the 14th European Conference on Artificial Intelligence (ECAI-00), 38-42
Weydert, EmilRankings in flux
In: Proceedings of the 3rd International Conference on Formal and Applied Practical Reasoning (FAPR-00), 37-48
Weydert, EmilThoughts on Evolving Science and Belief
In: Proceedings of the Workshop "Scientific Reasoning in AI and Philosophy of Science" at the 14th European Conference on Artificial Intelligence (ECAI-00), 62-69
1
Hide details for Electronic Proceedings ArticleElectronic Proceedings Article
Booth, RichardAttachment IconThe lexicographic closure as a revision process
In: Proceedings of the 8th International Workshop on Non-Monotonic Reasoning (NMR 2000), ?
20
Hide details for Journal ArticleJournal Article
Anderson, Penny
Basin, David A.
Program Development Schemata as Derived Rules
In: Journal of Symbolic Computation [30], 5-36
Bugliesi, Michele
Delzanno, Giorgio
Liquori, Luigi
Martelli, Maurizio
Object Calculi in Linear Logic
In: Journal of Logic and Computation [10], 75-104
de Nivelle, HansDeciding the E-plus class by an a posteriori, liftable order
In: Annals of Pure and Applied Logic [88], 219-232
de Nivelle, Hans
Hustadt, Ullrich
Schmidt, Renate A.
Resolution-Based Methods for Modal Logics
In: Logic Journal of the IGPL [8], 265-292
Degtyarev, Anatoli
Gurevich, Yuri
Narendran, Paliath
Veanes, Margus
Voronkov, Andrei
Decidability and Complexity of Simultaneous Rigid E-unification with One Variable and Related Results
In: Theoretical Computer Science [243], 167-184
Ganzinger, Harald
Jacquemard, Florent
Veanes, Margus
Rigid Reachability: The Non-Symmetric Form of Rigid E-unification
In: International Journal of Foundations of Computer Science [11], 3-27
Jaeger, ManfredAttachment IconOn the complexity of inference about probabilistic relational models
In: Artificial Intelligence [117], 297-308
Krishna Rao, M. R. K.Some characteristics of strong innermost normalization
In: Theoretical Computer Science [239], 141-164
Krishna Rao, M. R. K.Some classes of prolog programs inferable from positive data
In: Theoretical Computer Science [241], 211-223
Levy, Jordi
Veanes, Margus
On the Undecidability of Second-Order Unification
In: Information and Computation [159], 125-150
Lu, Mi
Wu, Jinzhao
On Theorem proving in Annotated Logics
In: Journal of Applied Non-Classical Logics [10], 121-143
Makinson, David
van der Torre, Leendert W. N.
Input-output logics
In: Journal of Philosophical Logic [29], 383-408
Matthews, Seán
Basin, David A.
Structuring Metatheory on Inductive Definitions
In: Information and Computation [162], 80-95
Müller, Martin
Niehren, Joachim
Podelski, Andreas
Ordering Constraints over Feature Trees
In: Constraints [5], 7-41
Sofronie-Stokkermans, VioricaAttachment IconDuality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. Part I
In: Studia Logica [64], 93-132
Sofronie-Stokkermans, VioricaAttachment IconDuality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. Part II
In: Studia Logica [64], 151-172
Sofronie-Stokkermans, VioricaAttachment IconPriestley Duality for SHn-algebras and Applications to the Study of Kripke-style Models for SHn-logics
In: Multiple-Valued Logic - An International Journal [5], 281-305
Talbot, Jean-MarcThe $\exists \forall^2$ fragment of the First-Order Theory of Set Constraints is $\pi^0_1$-hard
In: Information Processing Letters [74], 27-33
Talbot, Jean-Marc
Devienne, Philippe
Tison, Sophie
Generalized Definite Set Constraints
In: Constraints [5], 161-202
Veanes, MargusFarmer's Theorem Revisited
In: Information Processing Letters [74], 47-53
1
Hide details for Thesis - Masters thesisThesis - Masters thesis
Brinker, ChristofGeometrisches Schließen mit SPASS
Universität des Saarlandes
1
Hide details for Thesis - PhD thesisThesis - PhD thesis
Eisenbrand, FriedrichGomory-Chvátal Cutting planes and the Elementary Closure of Polyhedra
Universität des Saarlandes
1
Hide details for Thesis - Habilitation thesisThesis - Habilitation thesis
Weidenbach, ChristophEntscheidbarkeitsprobleme für monadische (Horn)Klauselklassen
Universität des Saarlandes, Naturwissenschaftlich-Technische Fakultät
61
Hide details for 19991999
6
Hide details for Part of a BookPart of a Book
Basin, David A.
Krieg-Brückner, Bernd
Formalization of the Development Process
In: Algebraic foundations of systems specification, 521-562
Bozzano, Marco
Delzanno, Giorgio
Martelli, Maurizio
Mascardi, Viviana
Zini, Floriano
Logic Programming and Multi-Agent Systems: a Synergic Combination for Applications and Semantics
In: The Logic Programming Paradigm: a 25-Year Perspective, 5-32
Nonnengart, Andreas
Szalas, Andrzej
A Fixpoint Approach to Second-Order Quantifier Elimination with Applications to Correspondence Theory
In: Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa, 18
van der Torre, Leendert W. N.
Tan, Yao-Hua
An update semantics for deontic reasoning
In: Norms, Logics and Information Systems: New Studies on Deontic Logic and Computer Science, 73-90
van der Torre, Leendert W. N.
Tan, Yao-Hua
Contextual Deontic Logic: violation contexts and factual defeasibility
In: Formal Aspects in Context, 173-192
Weydert, EmilJZBR - Iterated Belief Change for Conditional Ranking Constraints
In: Spinning Ideas - Electronic Essays Dedicated to Peter Gaerdenfors on His Fiftieth Birthday, 1-11
2
Hide details for ProceedingsProceedings
Ganzinger (ed.)Proceedings of the 16th International Conference on Automated Deduction (CADE-16)
Ganzinger, McAllester, Voronkov (ed.)Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR-99)
30
Hide details for Proceedings ArticleProceedings Article
Bozzano, Marco
Delzanno, Giorgio
Martelli, Maurizio
Mascardi, Viviana
Zini, Floriano
Multi-Agent Systems Development as a Software Engineering Enterprise
In: Proceedings of the 1st International Workshop on Practical Aspects of Declarative Languages (PADL-99), 46-60
Cortier, V.
Ganzinger, Harald
Jacquemard, Florent
Veanes, Margus
Decidable fragments of simultaneous rigid reachability
In: Proceedings of the 26th International Colloquium on Automata, Languages and Programming (ICALP-99), 250-260
de Nivelle, Hans
Areces, Carlos
de Rijke, Maarten
Prefixed Resolution: A Resolution Method for Modal and Description Logics
In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 187-201
Delzanno, Giorgio
Esparza, Javier
Podelski, Andreas
Constraint-Based Analysis of Broadcast Protocols
In: Proceedings of the 13th International Workshop on Computer Science Logic (CSL-99), 8th Annual Conference on the EACSL, 50-66
Delzanno, Giorgio
Podelski, Andreas
Model Checking in CLP
In: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS-99), 223-239
Eisenbrand, Friedrich
Schulz, Andreas S.
Bounds on the Chvátal Rank of Polytopes in the 0/1-Cube
In: Proceedings of the 7th Conference on Integer Programming and Combinatorial Optimization (IPCO-99), 137-150
Ganzinger, Harald
de Nivelle, Hans
Attachment IconA Superposition Decision Procedure for the Guarded Fragment with Equality
In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS-99), 295-303
Ganzinger, Harald
Meyer, Christoph
Veanes, Margus
The Two-Variable Guarded Fragment with Transitive Relations
In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS-99), 24-34
Hustadt, Ullrich
Schmidt, Renate A.
Maslov's Class K Revisited
In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 172-186
Hustadt, Ullrich
Schmidt, Renate A.
On the relation of resolution and tableaux proof systems for description logics
In: Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI-99), 110-115
Jaeger, ManfredAttachment IconFairness, Computable Fairness and Randomness
In: Proceedings of the 2nd International Workshop on Probabilistic Methods in Verification (PROBMIV-99), 57-66
Mukhopadhyay, Supratik
Podelski, Andreas
Attachment IconBeyond Region Graphs: Symbolic Forward Analysis of Timed Automata
In: Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS-99), 232-244
Podelski, Andreas
Charatonik, Witold
Müller, Martin
Set-based Failure Analysis for Logic Programs and Concurrent Constraint Programs
In: Programming Languages and Systems: Proceedings of the 8th European Symposium on Programming (ESOP-99), 177-192
Sofronie-Stokkermans, VioricaAttachment IconOn the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results
In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 157-171
Sofronie-Stokkermans, VioricaPriestley representation for distributive lattices with operators and applications to automated theorem proving
In: Dualities, Interpretability and Ordered Structures, 43-54
Sofronie-Stokkermans, VioricaRepresentation Theorems and Automated Theorem Proving in Non-Classical Logics
In: Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic (ISMVL-99), 242-247
Sofronie-Stokkermans, VioricaResolution-based theorem proving for non-classical logics based on distributive lattices with operators
In: Proceedings of the 11th International Congress of Logic, Methodology and Philosophy of Science. Volume of abstracts, 481-481
Sofronie-Stokkermans, Viorica
Stokkermans, Karel
Attachment IconModeling Interaction by Sheaves and Geometric Logic
In: Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99), 512-523
Stuber, JürgenTheory path orderings
In: Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99), 148-162
Talbot, Jean-Marc
Niehren, Joachim
Müller, Martin
Entailment of Atomic Set Constraints is PSPACE-Complete
In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS-99), 285-294
Tzakova, MiroslavaTableau Calculi for Hybrid Logics
In: Proceedings of the International Conference TABLEAUX'99 - Automated Reasoning with Analytic Tableaux and Related Methods, 278-292
van der Torre, Leendert W. N.Defeasible Goals
In: Proceedings of the 5th European Conference on Symbolic and Quantitative Approaches to Reasoning and Uncertainty (ECSQARU-99), 374-385
van der Torre, Leendert W. N.
Tan, Yao-Hua
An Update Semantics for Defeasible Obligations
In: Proceedings of the 15th Conference on Uncertainty in Artificial Intelligence (UAI-99), 631-638
van der Torre, Leendert W. N.
Tan, Yao-Hua
Rights, Duties and Commitments Between Agents
In: Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI-99), 1239-1244
Vorobyov, SergeiAttachment IconSubtyping Functional+Nonempty Record Types
In: Proceedings of the 12th International Workshop on Computer Science Logic (CSL-98), Annual Conference on the EACSL, 285-297
Waldmann, UweCancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups
In: Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR-99), 131-147
Weidenbach, ChristophTowards an Automatic Analysis of Security Protocols in First-Order Logic
In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 378-382
Weidenbach, Christoph
Afshordel, Bijan
Brahm, Uwe
Cohrs, Christian
Engel, Thorsten
Keen, Enno
Theobalt, Christian
Topić, Dalibor
System Description: SPASS Version 1.0.0
In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 314-318
Weydert, EmilJZBR - Iterated Belief Change for Conditional Ranking Constraints
In: Proceedings of the 4th Dutch-German Workshop on Nonmonotonic Reasoning Techniques and their Applications (DGNMR-99), 57-66
Weydert, Emil
van der Torre, Leendert W. N.
Risk parameters for utilitarian desires
In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI-99), Workshop on Practial Reasoning and Rationality, 48-54
15
Hide details for Journal ArticleJournal Article
Basin, David A.
Friedrich, Stefan
Modeling a Hardware Synthesis Methodology in Isabelle
In: Formal Methods in Systems Design [15], 99-122
Blackburn, Patrick
Tzakova, Miroslava
Hybrid Languages and Temporal Logic
In: Logic Journal of the IGPL [7], 27-54
Bockmayr, Alexander
Eisenbrand, Friedrich
Hartmann, Mark
Schulz, Andreas S.
On the Chvátal Rank of Polytopes in the 0/1 Cube
In: Discrete Applied Mathematics [98], 21-27
Buchmann, Johannes
Eisenbrand, Friedrich
On Factor Refinement in Number Fields
In: Mathematics of Computation [68], 345-350
Delzanno, Giorgio
Galmiche, Didier
Martelli, Maurizio
A specification logic for concurrent object-oriented programming
In: Mathematical Structures in Computer Science [9], 253-286
Eisenbrand, FriedrichOn the Membership Problem for the Elementary Closure of a Polyhedron
In: Combinatorica [19], 297-300
Gurevich, Yuri
Veanes, Margus
Logic with Equality: Partisan Corroboration and Shifted Pairing
In: Information and Computation [152], 205-235
Hustadt, Ullrich
Schmidt, Renate A.
An Empirical Analysis of Modal Theorem Provers
In: Journal of Applied Non-Classical Logics [9], 479-522
Madden, Peter
Bundy, Alan
Smaill, Alan
Recursive Program Optimization Through Inductive Synthesis Proof Transformation
In: Journal of Automated Reasoning [22], 65-115
Schmidt, Renate A.Decidability by Resolution for Propositional Modal Logics
In: Journal of Automated Reasoning [22], 379-396
van der Torre, Leendert W. N.
Tan, Yao-Hua
Contrary-to-duty reasoning with preference-based dyadic obligations
In: Annals of Mathematics and Artificial Intelligence [27], 49-78
van der Torre, Leendert W. N.
Tan, Yao-Hua
Diagnosis and Decision Making in Normative Reasoning
In: Journal of Artificial Intelligence and Law [7], 51-67
Voronkov, AndreiThe ground-negative fragment of first-order logics is $\pi^p_2$-complete
In: The Journal of Symbolic Logic [64], 984-990
Wang, YonggeRandomness, Stochasticity, and Approximation
In: Theory of Computing Systems [32], 517-529
Weidenbach, ChristophSPASS V0.95TPTP
In: Journal of Automated Reasoning [23], 21-21
3
Hide details for Thesis - Masters thesisThesis - Masters thesis
Fischmann, MatthiasOn Applications of Decidable Object-Oriented Type Theory
Universität des Saarlandes
Schmolzi, ChristianKooperative koevolutionäre Entwicklung von Fuzzy-Reglern
Universität des Saarlandes
Veit, JörgFormal Fairness Proofs for Optimistic Contract Signing Protocols
Universität des Saarlandes
5
Hide details for Thesis - PhD thesisThesis - PhD thesis
Baumeister, HubertAttachment IconRelations between Abstract Datatypes modeled as Abstract Datatypes
Universität des Saarlandes
Hustadt, UllrichResolution-Based Decision Procedures for Subclasses of First-Order Logic
Universität des Saarlandes
Meyer, ChristophSoft Typing for Clausal Inference Systems
Universität des Saarlandes
Stuber, JürgenAttachment IconSuperposition Theorem Proving for Commutative Algebraic Theories
Universität des Saarlandes
Tzakova, MiroslavaHybrid Languages
Universität des Saarlandes
73
Hide details for 19981998
5
Hide details for Part of a BookPart of a Book
Bachmair, Leo
Ganzinger, Harald
Equational Reasoning in Saturation-Based Theorem Proving
In: Automated Deduction: A Basis for Applications, 353-397
Schmidt, Renate A.Resolution is a Decision Procedure for Many Propositional Modal Logics
In: Advances in Modal Logic, Volume 1, 189-208
Stuber, JürgenSuperposition theorem proving for commutative rings
In: Automated Deduction - A Basis for Applications. Volume III. Applications, 31-55
Weidenbach, ChristophRechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197
Weidenbach, ChristophSorted Unification and Tree Automata
In: Automated Deduction - A Basis for Applications, 291-320
37
Hide details for Proceedings ArticleProceedings Article
Abdelwaheb, Ayari
Basin, David A.
Podelski, Andreas
LISA: A Specification Language Based on WS2S
In: Proceedings of the 11th International Workshop on Computer Science Logic (CSL-97), 18-34
Bachmair, Leo
Ganzinger, Harald
Strict Basic Superposition
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 160-174
Bachmair, Leo
Ganzinger, Harald
Voronkov, Andrei
Elimination of Equality via Transformation with Ordering Constraints
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 175-190
Basin, David A.
Matthews, Seán
Viganò, Luca
A Modular Presentation of Modal Logics in a Logical Framework
In: Proceedings of the 1st Tbilisi Symposium on Language, Logic and Computation: Selected Papers, 293-307
Blackburn, Patrick
Tzakova, Miroslava
A Hybrid Concept Language
In: Proceedings of the 5th International Symposium on Artificial Intelligence and Mathematics, ?
Bockmayr, Alexander
Dimopoulos, Yannis
Mixed Integer Programming Models for Planning Problems
In: Proceedings of the Workshop on Constraint Problem Reformulation (CP-98), 1-6
Charatonik, Witold
McAllester, David
Niwinski, Damian
Podelski, Andreas
Walukiewicz, Igor
The Horn Mu-calculus
In: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS-98), 58-69
Charatonik, Witold
Podelski, Andreas
Co-definite Set Constraints
In: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), 211-225
Charatonik, Witold
Podelski, Andreas
Directional Type Inference for Logic Programs
In: Proceedings of the 5th International Symposium in Static Analysis (SAS-98), 278-294
Charatonik, Witold
Podelski, Andreas
Set-Based Analysis of Reactive Infinite-state Systems
In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS-98), 358-375
Degtyarev, Anatoli
Gurevich, Yuri
Narendran, Paliath
Veanes, Margus
Voronkov, Andrei
The Decidability of Simultaneous Rigid E-Unification with One Variable
In: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), 181-195
Delzanno, GiorgioSpecification of Term Rewriting in Linear Logic
In: Proceedings of Workshop on Proof-Search in Type-Theoretic Languages, ??
Firozabadhi, Babak Sadighi
van der Torre, Leendert W. N.
Towards a formal analysis of control systems
In: Proceedings of the 13th European Conference on Artificial Intelligence (ECAI-98), 317-318
Ganzinger, Harald
Jacquemard, Florent
Veanes, Margus
Rigid Reachability
In: Proceedings of the 4th Asian Computing Science Conference on Advances in Computing Science (ASIAN-98), 4-21
Hustadt, Ullrich
Schmidt, Renate A.
Simplification and backjumping in modal tableau
In: Proceedings of the International Conference on Automated Reaso ning with Analytic Tableaux and Related Methods (TABLEAUX'98), 187-201
Hustadt, Ullrich
Schmidt, Renate A.
Weidenbach, Christoph
Optimised Functional Translation and Resolution
In: Proceedings of the International Conference on Automated Reaso ning with Analytic Tableaux and Related Methods (TABLEAUX'98), 36-37
Jacquemard, Florent
Meyer, Christoph
Weidenbach, Christoph
Unification in Extensions of Shallow Equational Theories
In: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), 76-90
Jaeger, ManfredAttachment IconConvergence Results for Relational Bayesian Networks
In: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS-98), 44-55
Jaeger, ManfredAttachment IconMeasure Selection: Notions of Rationality and Representation Independence
In: Proceedings of the 14th Conference on Uncertainty in Artificial Intelligence (UAI-98), 274-281
Jaeger, ManfredAttachment IconReasoning About Infinite Random Structures with Relational Bayesian Networks
In: Proceedings of the 6th International Conference on Principles of Knowledge Representation and Reasoning (KR-98), 570-581
Nonnengart, Andreas
Rock, Georg
Weidenbach, Christoph
On Generating Small Clause Normal Forms
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 397-411
Schmidt, Renate A.E-Unification for Subsystems of S4
In: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), 106-120
Sofronie-Stokkermans, VioricaOn Translation of Finitely-Valued Logics to Classical First-Order Logic
In: Proceedings of the 13th European Conference on Artificial Intelligence (ECAI-98), 410-411
Sofronie-Stokkermans, VioricaRepresentation Theorems and Automated Theorem Proving in Certain Classes of Non-Classical Logics
In: Proceedings of the Workshop on Many-Valued Logic for AI Applications (ECAI-98), ?-?
van der Torre, Leendert W. N.Labeled logics of conditional goals
In: Proceedings of the 13th European Conference on Artificial Intelligence (ECAI-98), 368-369
van der Torre, Leendert W. N.Phased labeled logics of conditional goals
In: Proceedings of the 6th European Workshop on Logics in AI: Logics in Artificial Intelligence (JELIA-98), 92-106
van der Torre, Leendert W. N.
Tan, Yao-Hua
An update semantics for prima facie obligations
In: Proceedings of the 13th European Conference on Artificial Intelligence (ECAI-98), 38-42
van der Torre, Leendert W. N.
Tan, Yao-Hua
Prohairetic Deontic Logic (PDL)
In: Proceedings of the 6th European Workshop on Logics in AI: Logics in Artificial Intelligence (JELIA-98), 77-91
van der Torre, Leendert W. N.
Tan, Yao-Hua
The temporal analysis of Chisholm's paradox
In: Proceedings of the 15th National Conference, and 10th Conference on Innovative Applications of Artificial Intelligence (AAAI-98) and (IAAI-98), 650-655
Veanes, MargusThe Relation Between Second-Order Unification and Simultaneous Rigid E-Unification
In: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS-98), 264-275
Vorobyov, SergeiAttachment Icon$\forall\exists^\ast$-Equational Theory of Context Unification is $\Pi_1^0$-Hard
In: Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS-98), 597-606
Vorobyov, Sergei
Voronkov, Andrei
Attachment IconComplexity of Nonrecursive Logic Programs with Complex Values
In: Proceedings of the 17th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS-98), 244-253
Waldmann, UweSuperposition for Divisible Torsion-Free Abelian Groups
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 144-159
Weydert, EmilMinimal information entailment : A preliminary account
In: Proceedings of the 7th International Workshop on Nonmonotonic Reasoning (Workshop on Formal Aspects and Applications of Nonmonotonic Reasoning), 64-72
Weydert, EmilSystem JZ : How to build a canonical ranking model of a default knowledge base
In: Proceedings of the 6th International Conference on Principles of Knowledge Representation and Reasoning (KR-98), 190-201
Weydert, Emil
van der Torre, Leendert W. N.
Goals, desires, utilities and preferences
In: Proceedings of the ECAI-98 Workshop : Decision theory meets artificial intelligence - qualitative and quantitative approaches, 57-64
Wu, Jinzhao
Lu, Mi
CWA in Multi-Valued Logics
In: Proceedings of the 3rd Asian Symposium on Computer Mathematics (ASCM-98), 259-270
22
Hide details for Journal ArticleJournal Article
Bachmair, Leo
Ganzinger, Harald
Ordered Chaining Calculi for First-Order Theories of Transitive Relations
In: Journal of the ACM [45], 1007-1049
Barth, Peter
Bockmayr, Alexander
Modelling Discrete Optimisation Problems in Constraint Logic Programming
In: Annals of Operations Research [81], 467-496
Basin, David A.
Klarlund, Nils
Automata Based Symbolic Reasoning in Hardware Verification
In: Formal Methods in Systems Design [13], 255-288
Basin, David A.
Matthews, Seán
Viganò, Luca
Labelled Modal Logics: quantifiers
In: Journal of Logic, Language and Information [7], 237-263
Basin, David A.
Matthews, Seán
Viganò, Luca
Natural Deduction for Non-Classical Logics
In: Studia Logica [60], 119-160
Blackburn, Patrick
Tzakova, Miroslava
Hybrid Completeness
In: Logic Journal of the IGPL [6], 625-650
Blackburn, Patrick
Tzakova, Miroslava
Hybridizing Concept Languages
In: Annals of Mathematics and Artificial Intelligence [24], 23-49
Bockmayr, Alexander
Kasper, Thomas
Branch-and-Infer: A Unifying Framework for Integer and Finite Domain Constraint Programming
In: INFORMS Journal on Computing [10], 287-300
Charatonik, WitoldAn Undecidable Fragment of the Theory of Set Constraints
In: Information Processing Letters [68], 147-151
Charatonik, WitoldSet Constraints in Some Equational Theories
In: Information and Computation [142], 40-75
Frank, Ian
Basin, David A.
Search in Games with Incomplete Information: A Case Study Using Bridge Card Play
In: Artificial Intelligence [100], 87-123
Ganzinger, HaraldPreface
In: Theoretical Computer Science [208], 1
Krishna Rao, M. R. K.Modular Aspects of term graph rewriting
In: Theoretical Computer Science [208], 59-86
Letz, Reinhold
Weidenbach, Christoph
Paradigmen und Perspektiven der automatischen Deduktion
In: KI, Organ des Fachbereichs 1 "Künstliche Intelligenz'' der Gesellschaft für Informatik e.V. [4], 15-19
Matthews, Seán
Basin, David A.
Scoped Metatheorems
In: Electronic Notes in Computer Science [15], 1-14
Nonnengart, AndreasModal Frame Characterization by Way of Auxiliary Modalities
In: Logic Journal of the IGPL [6], 875-899
Stuber, JürgenSuperposition theorem proving for abelian groups represented as integer modules
In: Theoretical Computer Science [208], 149-177
Waldmann, UweExtending reduction orderings to ACU-compatible reduction orderings
In: Information Processing Letters [67], 43-49
Weidenbach, Christoph
Meyer, Christoph
Cohrs, Christian
Engel, Thorsten
Keen, Enno
SPASS V0.77
In: Journal of Automated Reasoning [21], 113-113
Werner, Andreas
Bockmayr, Alexander
Krischer, Stefan
How to realize LSE narrowing
In: New Generation Computing [16], 397-434
Wu, Jinzhao
Liu, Zhuojun
Well-Behaved Inference Rules for First-Order Theorem Proving
In: Journal of Automated Reasoning [21], 381-400
Wu, Jinzhao
Tan, Hongyan
Li, Yongli
An Algebraic Method to Decide the Deduction Problem in Many-Valued Logics
In: Journal of Applied Non-Classical Logics [8], 353-360
2
Hide details for ReportReport
Blackburn, Patrick
Tzakova, Miroslava
Hybrid Languages and Temporal Logic (Full Version)
Sofronie-Stokkermans, VioricaAttachment IconResolution-based Theorem Proving for SHn-Logics
3
Hide details for Thesis - Masters thesisThesis - Masters thesis
Althaus, ErnstBerechnung optimaler Steinerbäume in der Ebene
Universität des Saarlandes
Friedrich, StefanIntegration of a Decision Procedure for Second-Order Monadic Logic in a Higher-Order Logic Theorem Proving Environment
Universität des Saarlandes
Leven, PeterIntegrating Clausal Decision Procedures in a Tactic Based Theorem Prover
Universität des Saarlandes
2
Hide details for Thesis - PhD thesisThesis - PhD thesis
Kasper, ThomasA Unifying Logical Framework for Integer Linear Programming and Finite Domain Constraint Programming
Universität des Saarlandes
Struth, GeorgCanonical Transformation in Algebra, Universal Algebra and Logic
Universität des Saarlandes
1
Hide details for Thesis - Habilitation thesisThesis - Habilitation thesis
Podelski, AndreasThema der Antrittsvorlesung: Alte Resultate aus der Automatentheorie
Universität des Saarlandes
1
Hide details for MiscellaneousMiscellaneous
Weydert, EmilSome Notes on Nonmonotonic Probabilistic Inference
42
Hide details for 19971997
1
Hide details for BookBook
Gabbay, Kruse, Nonnengart, Ohlbach (ed.)Qualitative and Quantitative Practical Reasoning
1
Hide details for ProceedingsProceedings
Weydert, Brewka, Witteveen (ed.)Proceedings of the 3rd Dutch/German Workshop on Nonmonotonic Reasoning Techniques and their Applications (DGNMR-97)
24
Hide details for Proceedings ArticleProceedings Article
Barth, Peter
Bockmayr, Alexander
PLAM: ProLog and Algebraic Modelling
In: Proceedings of the 5th International Conference on the Practical Application of Prolog, 73-82
Basin, David A.
Matthews, Seán
Viganò, Luca
A New Method for Bounding the Complexity of Modal Logics
In: Proceedings of the 5th Kurt Gödel Colloquium on Computational Logic and Proof Theory (KGC-97), 89-102
Basin, David A.
Matthews, Seán
Viganò, Luca
Labelled quantified modal logics
In: Proceedings of the 21st Annual German Conference on Artificial Intelligence (KI-97): Advances in Artificial Intelligence, 171-182
Charatonik, Witold
Podelski, Andreas
Set Constraints with Intersection
In: Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS-97), 362-372
Ganzinger, Harald
Meyer, Christoph
Weidenbach, Christoph
Soft Typing for Ordered Resolution
In: Proceedings of the 14th International Conference on Automated Deduction (CADE-14), 321-335
Hopf, JörnCooperative Coevolution of Fuzzy Rules
In: Proceedings of the 2nd International ICSC Symposium on Fuzzy Logic and Applications (ISFL-97), 337-381
Hustadt, Ullrich
Schmidt, Renate A.
On Evaluating Decision Procedures for Modal Logics
In: Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI-97), 202-207
Jaeger, ManfredAttachment IconRelational Bayesian Networks
In: Proceedings of the 13th Conference of Uncertainty in Artificial Intelligence (UAI-13), 266-273
Matthews, SeánA practical implementation of simple consequence relations using inductive definitions
In: Proceedings of the 14th International Conference on Automated Deduction (CADE-14), 306-320
Matthews, SeánExtending a logical framework with a modal connective for validity
In: Proceedings of the 3rd Symposium on Theoretical Aspects of Computer Software (TACS-97), 491-514
Müller, Martin
Niehren, Joachim
Podelski, Andreas
Inclusion Constraints over Non-empty Sets of Trees
In: Proceedings of the 7th International Joint Conference CAAP/FASE: Theory and practice of software development (TAPSOFT-97), 345-356
Müller, Martin
Niehren, Joachim
Podelski, Andreas
Ordering Constraints over Feature Trees
In: Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming (CP-97), 549-562
Pacholski, Leszek
Podelski, Andreas
Set Constraints: a Pearl in Research on Constraints
In: Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming (CP-97), 549-562
Podelski, AndreasSet-Based Analysis of Logic Programs and Reactive Logic Programs
In: Proceedings of the International Symposium on Logic Programming (ILPS-14), 35-36
Struth, GeorgOn the Word Problem for Free Lattices
In: Proceedings of the 8th International Conference on Rewriting Techniques and Applications (RTA-97), 128-141
Stuber, JürgenStrong Symmetrization, Semi-Compatibility of Normalized Rewriting and First-Order Theorem Proving
In: Proceedings of the International Workshop on First-Order Theorem Proving (FTP-97), 125-129
van der Torre, Leendert W. N.
Tan, Yao-Hua
Distinguishing different roles in normative reasoning
In: Proceedings of the 6th International Conference on Artificial Intelligence and Law (ICAIL-97), 225-232
van der Torre, Leendert W. N.
Tan, Yao-Hua
Reasoning about exceptions
In: Proceedings of the 21st Annual German Conference on Artificial Intelligence (KI-97): Advances in Artificial Intelligence, 405-408
Vorobyov, SergeiThe first-order theory of one step rewriting in linear noetherian systems is undecidable
In: Proceedings of the 8th International Conference on Rewriting Techniques and Applications (RTA-97), 254-268
Vorobyov, SergeiThe `hardest´ natural decidable theory
In: Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS-97), 294-305
Waldmann, UweA Superposition Calculus for Divisible Torsion-Free Abelian Groups
In: Proceedings of the International Workshop on First-Order Theorem Proving (FTP-97), 130-134
Wang, YonggeRandomization and Approximation Techniques in Computer Science
In: Proceedings of the International Workshop on Randomization and Approximation Techniques in Computer Science (RANDOM-97), 209-225
Weydert, EmilQualitative Entropy Maximization - A preliminary report
In: Proceedings of the 3rd Dutch/German Workshop on Nonmonotonic Reasoning Techniques and their Applications (DGNMR-97), 63-72
Weydert, EmilRational Default Quantifier Logic
In: Proceedings of the 1st International Joint Conference on Qualitative and Quantitative Practical Reasoning (ESQARU-FAPR-97), 589-600
8
Hide details for Journal ArticleJournal Article
Basin, David A.
Matthews, Seán
Viganò, Luca
Labelled Propositional Modal Logics: Theory and Practice
In: Journal of Logic and Computation [7], 685-717
Krishna Rao, M. R. K.A framework for incremental learning of logic programs
In: Theoretical Computer Science [185], 191-213
Nivat, Maurice
Podelski, Andreas
Minimal Ascending and Descending Tree Automata
In: SIAM Journal on Computing [26], 39-58
Ohlbach, Hans Jürgen
Schmidt, Renate A.
Functional Translation and Second-Order Frame Properties of Modal Logics
In: Journal of Logic and Computation [7], 581-603
Podelski, Andreas
Smolka, Gert
Situated Simplification
In: Theoretical Computer Science [173], 235-252
Rahman, Shahid
Rückert, Helge
Fischmann, Matthias
Dialogues and Ontology, the Dialogical Approach to Free Logic
In: Logique et Analyse [160], 357-374
Wang, YonggeNP-hard sets are superterse unless NP is small
In: Information Processing Letters [61], 1-6
Weidenbach, ChristophSPASS Version 0.49
In: Journal of Automated Reasoning [18], 247-252
4
Hide details for Thesis - Masters thesisThesis - Masters thesis
Christen, MichaelAttachment IconA Calculus of Simplification for Superposition
Universität des Saarlandes
Naumann, StefanIntegration des automatischen Beweisers SPASS in die mathematische Assistenzumgebung OMEGA
Universität des Saarlandes
Rau, RainerAdaption of a Fuzzy Controller for a Cybernetic System through an Evolutionary Algorithm
Universität des Saarlandes
Timm, Jan-GeorgAttachment IconTesting the Satisfiability of RPO Constraints
Universität des Saarlandes
4
Hide details for Thesis - PhD thesisThesis - PhD thesis
Schmidt, Renate A.Optimised Modal Translation and Resolution
Universität des Saarlandes
Viganò, LucaA Framework for Non-Classical Logics
Universität des Saarlandes
Waldmann, UweCancellative Abelian Monoids in Refutational Theorem Proving
Universität des Saarlandes
Zeyer, JörgEine Beobachtungs-Logik für modulare Sprachen
Universität des Saarlandes
64
Hide details for 19961996
1
Hide details for BookBook
Graf, PeterTerm Indexing
6
Hide details for Part of a BookPart of a Book
Basin, David A.
Matthews, Seán
Viganò, Luca
A Topography of Labelled Modal Logics
In: Frontiers of Combining Systems (First International Workshop, Munich, March 1996), 75-92
Basin, David A.
Walsh, Toby
A Calculus for and Termination of Rippling
In: Automated mathematical induction, 147-180
Kraan, Ina
Basin, David A.
Bundy, Alan
Middle-Out Reasoning for Synthesis and Induction
In: Automated mathematical induction, 113-145
Matthews, Seán
Simpson, Alex
Reflection using the derivability conditions
In: Logic and Algebra, 603-616
Ohlbach, Hans Jürgen
Schmidt, Renate A.
Hustadt, Ullrich
Translating Graded Modalities into Predicate Logic
In: Proof Theory of Modal Logic, 253-291
Weydert, EmilDoxastic Normality Logic: A Qualitative Probabilistic Modal Framework for Defaults and Belief
In: Logic, Action, and Information, 152-171
1
Hide details for ProceedingsProceedings
Ganzinger (ed.)Rewriting Techniques and Applications, 7th International Conference, RTA-96
35
Hide details for Proceedings ArticleProceedings Article
Ayari, Abdelwaheb
Basin, David A.
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
Barth, Peter
Bockmayr, Alexander
Modelling 0-1 Problems in CLP($\cal PB$)
In: Proceedings of the Second International Conference on Practical Application of Constraint Technology, 1-9
Basin, David A.
Friedrich, Stefan
Modeling a hardware synthesis methodology in Isabelle
In: Theorem Proving in Higher Order Logics. 9th International Conference, TPHOLs'96, 33-50
Basin, David A.
Ganzinger, Harald
Complexity Analysis Based on Ordered Resolution
In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS'96), 456-465
Basin, David A.
Matthews, Seán
Structuring metatheory on inductive definitions
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 171-185
Basin, David A.
Matthews, Seán
Viganò, Luca
Implementing Modal and Relevance Logics in a Logical Framework
In: Proceedings of the 5th International Conference on Principles of Knowledge Representation and Reasoning (KR'96), 386-397
Bockmayr, AlexanderConstraints in functional logic programming (Abstract)
In: Integration of functional and logic languages, 4
Bockmayr, Alexander
Barth, Peter
Kasper, Thomas
Methods and Tools for Pseudo-Boolean Problems
In: 2. Workshop Boolesche Probleme, 105-109
Bockmayr, Alexander
Kasper, Thomas
Pseudo-Boolean and Finite Domain Constraint Programming: A Case Study
In: Deklarative Constraint Programmierung, 29-41
Cantu, Francisco
Bundy, Alan
Smaill, Alan
Basin, David A.
Experiments in Automating Hardware Verification using Inductive Proof Planning
In: Proceedings of the Formal Methods for Computer-Aided Design Conference (FMCAD'96), 94-108
Charatonik, Witold
Podelski, Andreas
The Independence Property of a Class of Set Constraints
In: Principles and Practice of Constraint Programming, Proceedings of the Second International Conference (CP'96), 76-90
Ganzinger, HaraldSaturation-based theorem proving (abstract)
In: Automata, Languages and Programming: International Colloquium (ICALP-23), 1-3
Ganzinger, Harald
Waldmann, Uwe
Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 388-402
Graf, PeterPath indexing for AC-theories
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 718-732
Graf, Peter
Meyer, Christoph
Advanced indexing operations on substitution trees
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 553-567
Hopf, Jörn
Rau, Rainer
Decision Making in an Economy Exploiting Fuzzy Rules Obtained from a Genetic Algorithm
In: Soft Computing with Industrial Applications, 331-336
Jaeger, ManfredRepresentation Independence of Nonmonotonic Inference Relations
In: Principles of Knowledge Representation and Reasoning, Proceedings of the 5th International Conference (KR-96), 461-472
Jaeger, Manfred
Mannila, Heikki
Weydert, Emil
Data Mining as Selective Theory Extraction in Probabilistic Logic
In: Proceedings of the 1996 SIGMOD Workshop on Research Issues in Data Mining and Knowledge Discovery, -
Krishna Rao, M. R. K.A class of Prolog programs inferable from positive data
In: Algorithmic Learning Theory, 272-284
Krishna Rao, M. R. K.Completeness results for basic narrowing in non-copying implementations
In: Logic Programming, 393-407
Krishna Rao, M. R. K.Learning Prolog programs from examples
In: Knowledge Based Computer Systems, 19-30
Krishna Rao, M. R. K.Modularity of termination in term graph rewriting
In: Rewriting Techniques and Applications, 230-244
Krishna Rao, M. R. K.Some characteristics of strong innermost normalization
In: Algebraic Methodology and Software Technology, 5th International Conference, AMAST '96, 406-420
Matthews, SeánImplementing $\textrm FS_0$ in Isabelle: Adding Structure at the Metalevel
In: Design and Implementation of Symbolic Computation Systems (DISCO'96), 228-239
Nonnengart, AndreasResolution-Based Calculi for Modal and Temporal Logics
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 598-612
Ohlbach, Hans JürgenSCAN-Elimination of Predicate Quantifiers
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 161-165
Stuber, JürgenSuperposition Theorem Proving for Abelian Groups Represented as Integer Modules
In: Rewriting Techniques and Applications, 7th International Conference, RTA-96, 33-47
Vorobyov, SergeiAn improved lower bound for the elementary theories of trees
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 275-287
Vorobyov, SergeiOn the bounded theories of finite trees
In: Second Asian Computing Science Conference, ASIAN'96, 152-161
Weidenbach, ChristophSorted Unification and Its Application to Automated Theorem Proving
In: Proceedings of the CADE-13 Workshop: Term Schematizations and Their Applications, 67-76
Weidenbach, ChristophUnification in Pseudo-Linear Sort Theories is Decidable
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 343-357
Weidenbach, ChristophUnification in Sort Theories
In: Proceedings of the 10th International Workshop on Unification, UNIF'96, 16-25
Weidenbach, Christoph
Gaede, Bernd
Rock, Georg
SPASS & FLOTTER, Version 0.42
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 141-145
Weydert, EmilDefault Quantifier Logic
In: Proceedings of the ECAI'96 Workshop on Integrating Nonmonotonicity into Automated Reasoning Systems, -
Weydert, EmilSystem J - Revision Entailment: Default Reasoning through Ranking Measure Updates
In: Practical Reasoning - International Conference on Formal and Applied Practical Reasoning, FAPR'96, 637-649
7
Hide details for Journal ArticleJournal Article
Basin, David A.
Matthews, Seán
Adding Metatheoretic facilities to First-order Theories
In: Journal of Logic and Computation [6], 835-849
Basin, David A.
Walsh, Toby
A Calculus for and Termination of Rippling
In: Journal of Automated Reasoning [16], 147-180
Chaudhuri, Shiva
Dimopoulos, Yannis
Zaroliagis, Christos
On the Parallel Complexity of Acyclic Logic Programs
In: Parallel Processing Letters [6], 223-230
Dimopoulos, YannisOn Computing Logic Programs
In: Journal of Automated Reasoning [17], 259-289
Kraan, Ina
Basin, David A.
Bundy, Alan
Middle-out reasoning for synthesis and induction
In: Journal of Automated Reasoning [16], 113-145
Krishna Rao, M. R. K.Relating confluence, innermost-confluence and outermost-confluence properties of term rewriting systems
In: Acta Informatica [33], 595-606
Weidenbach, ChristophUnification in Sort Theories and its Applications
In: Annals of Mathematics and Artificial Intelligence [18], 261-293
6
Hide details for ReportReport
Claus, Hopf, Schwefel (ed.)Evolutionary Algorithms and their Application
Frank, Ian
Basin, David A.
Search in Games with Incomplete Information: A Case Study Using Bridge Card Play
Hähnle, Reiner
Kerber, Manfred
Weidenbach, Christoph
Common Syntax of the DFG-Schwerpunktprogramm ``Deduktion''
Hopf, JörnOptimizing Photo Mask Layout for Grey-tone Lithography
Hopf, JörnOptimizing Photo Mask Layout for Grey-tone Lithography
Ohlbach, Hans Jürgen
Koehler, Jana
Reasoning about Sets via Atomic Decomposition
6
Hide details for Thesis - Masters thesisThesis - Masters thesis
Autexier, SergeHeuristiken zum Beweisen von Gleichungen
Universität des Saarlandes
Bach, AlexanderAttachment IconStatic analysis of functional programs via Linear Logic
Universität des Saarlandes
Engel, ThorstenAttachment IconQuantifier Elimination in Second-Order Predicate Logic
Universität des Saarlandes
Meyer, ChristophAttachment IconParallel Unit Resulting Resolution
Universität des Saarlandes
Schlobach, StefanUntersuchung nicht-monotoner Logiken - Fallstudie zur Automatisierung
Universität des Saarlandes
Smaus, Jan-GeorgFinding Resolution K-Transformations
Universität des Saarlandes
1
Hide details for Thesis - PhD thesisThesis - PhD thesis
Weidenbach, ChristophComputational Aspects of a First-Order Logic with Sorts
Universität des Saarlandes
1
Hide details for Thesis - Habilitation thesisThesis - Habilitation thesis
Bockmayr, AlexanderGleichheit und Constraints in der Logikprogrammierung
Universität des Saarlandes
55
Hide details for 19951995
1
Hide details for BookBook
Barth, PeterLogic-based 0-1 constraint programming
1
Hide details for Part of a BookPart of a Book
Hustadt, UllrichIntroducing Epistemic Operators into a Description Logic
In: Knowledge and Belief in Philosophie and Artificial Intelligence, 65-85
1
Hide details for ProceedingsProceedings
Podelski (ed.)Constraint Programming: Basics and Trends
In: Constraint Programming: Basics and Trends, 328
28
Hide details for Proceedings ArticleProceedings Article
Anderson, Penny
Basin, David A.
Deriving and Applying Logic Program Transformers
In: Algorithms, Concurrency and Knowledge (1995 Asian Computing Science Conference), 301-318
Ayari, Abdelwaheb
Basin, David A.
Interpretation of the Deductive Tableau in HOL
In: Proceedings of the First Isabelle Users Workshop, 91-100
Bachmair, Leo
Ganzinger, Harald
Associative-Commutative Superposition
In: Proceedings of the 4th International Workshop on Conditional and Typed Rewrite Systems (CTRS-94), 1-14
Bachmair, Leo
Ganzinger, Harald
Stuber, Jürgen
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
Barth, Peter
Bockmayr, Alexander
Finite domain and cutting plane techniques in CLP($\cal PB$)
In: Proceedings of the Twelfth International Conference on Logic Programming, 133-147
Barth, Peter
Kleine Büning, Hans
Weidenbach, Christoph
Workshop CPL Computational Propositional Logic
In: KI-95 Activities: Workshops, Posters, Demos, 71-72
Basin, David A.
Klarlund, Nils
Hardware Verification using Monadic Second-Order Logic
In: Proceedings of the 7th International Conference on Computer-Aided Verification (CAV '95), 31-41
Baumeister, HubertRelations as Abstract Datatypes: An Institution to Specify Relations between Algebras
In: Proceedings of the 6th Joint Conference on Theory and Practice of Software Development (TAPSOFT '95), 756-771
Bockmayr, AlexanderSolving pseudo-Boolean constraints
In: Constraint Programming: Basics and Trends, 22-38
Bockmayr, Alexander
Werner, Andreas
LSE narrowing for decreasing conditional term rewrite systems
In: Conditional Term Rewriting Systems CTRS'94, 51-70
Bundy, Alan
Lombart, V.
Relational Rippling: a General Approach
In: Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence (IJCAI-95), 175-181
Graf, PeterSubstitution Tree Indexing
In: Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95), 117-131
Hanus, MichaelOn Extra Variables in (Equational) Logic Programming
In: Proceedings of the Twelfth International Conference on Logic Programming, 665-679
Jaeger, ManfredMinimum Cross-Entropy Reasoning: A Statistical Justification
In: Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence (IJCAI-95), 1847-1852
Krishna Rao, M. R. K.Graph reducibility of term rewriting systems
In: Proceedings of Mathematical Foundations of Computer Science, 371-381
Krishna Rao, M. R. K.Incremental Learning of Logic Programs
In: Proceedings of International Workshop on Algorithmic Learning Theory, 95-109
Krishna Rao, M. R. K.Semi-completeness of Hierarchical and Super-hierarchical Combinations of Term Rewriting Systems
In: Proceedings of the 6th Joint Conference on Theory and Practice of Software Development, 379-393
Krishna Rao, M. R. K.
Shyamasundar, R. K.
Unification-free Execution of Well-moded Prolog Programs
In: Proc. of International Static Analysis Symposium, 243-260
Madden, PeterProgram improvement by proof planning
In: Proceedings of British Colloquium on Theoretical Computer Science (BCTCS 11),
Madden, Peter
Green, Ian
A General Technique for Automatic Optimization by Proof Planning
In: Proceedings of the 2nd International Conference on Artificial Intelligence and Symbolic Mathematical Computing (AISMC-2), 80-96
Ohlbach, Hans Jürgen
Schmidt, Renate A.
Hustadt, Ullrich
Symbolic Arithmetical Reasoning with Qualified Number Restrictions
In: Proceedings of International Workshop on Description Logics'95, 89-95
Podelski, Andreas
Smolka, Gert
Operational Semantics of Constraint Logic Programming with Coroutining
In: Proceedings of the 12th International Conference on Logic Programming, 449-463
Podelski, Andreas
Smolka, Gert
Situated Simplification
In: Proceedings of the First International Conference on Principles and Practice of Constraint Programming (CP'95), 328-344
Vorobyov, SergeiFsub with recursive types: `Types-As-Propositions´ Interpretations in M. Rabin's S2S
In: Proceedings of JFLA'95: Journées Francophones des Langages Applicatifs (JFLA'95), 49-73
Vorobyov, SergeiStructural decidable extensions of bounded quantification
In: Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (POPL'95), 164-175
Weydert, EmilDefault Entailment. A preferential construction semantics for defeasible inference
In: Advances in Artificial Intelligence: Proceedings of the 19th German Annual Conference on Artificial Intelligence, 173-184
Weydert, EmilDefaults and Infinitesimals. Defeasible inference by nonarchimedean entropy maximization
In: Proceedings of the 11th Conference on Uncertainty in Artificial Intelligence (UAI 95), 540-547
Weydert, EmilNumeric Defaults. About an expressive first-order framework for reasoning with infinitesimal probabilities
In: Symbolic and Quantitative Approaches to Reasoning and Uncertainty (ECSQARU 95), 420-427
9
Hide details for Journal ArticleJournal Article
Baader, Franz
Ohlbach, Hans Jürgen
A Multi-Dimensional Terminological Knowledge Representation Language
In: Journal of Applied Non-Classical Logics [5], 153-198
Bachmair, Leo
Ganzinger, Harald
Lynch, Christopher
Snyder, Wayne
Basic Paramodulation
In: Information and Computation [121], 172-192
Barth, Peter
Bockmayr, Alexander
Pseudo-Boolean Constraint Logic Programming
In: Computational Logic. The Newsletter of the European Network in Computational Logic [2], 52-53
Bockmayr, Alexander
Krischer, Stefan
Werner, Andreas
Narrowing strategies for arbitrary canonical systems
In: Fundamenta Informaticae [24], 125-155
Hanus, MichaelAnalysis of Residuating Logic Programs
In: Journal of Logic Programming [24], 219-245
Hanus, MichaelCompile-Time Analysis of Nonlinear Constraints in CLP(R)
In: New Generation Computing [13], 155-186
Krishna Rao, M. R. K.Modular Proofs for Completeness of hierarchical term rewriting systems
In: Theoretical Computer Science [151], 487-512
Ohlbach, Hans Jürgen
Weidenbach, Christoph
A Note on Assumptions about Skolem Functions
In: Journal of Automated Reasoning [15], 267-275
Weidenbach, ChristophFirst-Order Tableaux with Sorts
In: Journal of the Interest Group in Pure and Applied Logics [3], 887-906
7
Hide details for Thesis - Masters thesisThesis - Masters thesis
Ayari, AbdelwahebAttachment IconA Reinterpretation of the Deductive Tableaux System in Higher-Order Logic
Universität des Saarlandes
Bozkurt, AhmetStrategien für Resolutionsbeweiser in Logik höherer Stufe
Universität des Saarlandes
Gaede, BerndAttachment IconSuperposition Extended with Sorts
Universität Kaiserslautern
Gerber, ChristianEntwicklung eines Algorithmus zur effizienten Anfragebeantwortung für eine terminologische Wissensrepräsentationssprache
Universität des Saarlandes
Klotzki, PiaWiedemann-Algorithmus zur Lösung dünnbesetzter Gleichungssysteme über Fp
Universität des Saarlandes
Mohr, ErikResolution-Based Calculi for Modal Logics
Universität des Saarlandes
Rock, GeorgAttachment IconTransformations of First-Order Formulae for Automated Reasoning
Universität des Saarlandes
5
Hide details for Thesis - PhD thesisThesis - PhD thesis
Barth, PeterLogic-based 0-1 Constraint Solving in Constraint Logic Programming
Fachbereich Informatik, Universität des Saarlandes, Germany
Fehrer, DetlefA unifying logical framework for reason maintenance
Universität des Saarlandes
Graf, PeterTerm Indexing
Universität des Saarlandes
Jaeger, ManfredDefault Reasoning about Probabilities
Universität des Saarlandes
Nonnengart, AndreasA Resolution-Based Calculus for Temporal Logics
Universität des Saarlandes
1
Hide details for Thesis - Habilitation thesisThesis - Habilitation thesis
Basin, David A.Thema der Antrittsvorlesung: MONA - Ein Werkzeug zur Systemverifikation und -entwicklung
Universität des Saarlandes
2
Hide details for Unpublished/DraftUnpublished/Draft
Ohlbach, Hans JürgenBoolean Algebras with Functions - Correspondence, Completeness and Quantifier Elimination
Ohlbach, Hans JürgenClause Killer Transformations
64
Hide details for 19941994
2
Hide details for Part of a BookPart of a Book
Hopf, Jörn
Klawonn, Frank
Learning the Rule Base of a Fuzzy Controller by a Genetic Algorithm
In: Fuzzy Systems in Computer Science, 63-74
Matthews, SeánA Theory and its Metatheory in $FS_0$
In: What is a logical system?, 329-354
1
Hide details for ProceedingsProceedings
Gabbay, Ohlbach (ed.)Temporal Logic: Proceedings of the 1st International Conference on Temporal Logic
43
Hide details for Proceedings ArticleProceedings Article
Antoy, Sergio
Echahed, Rachid
Hanus, Michael
A Needed Narrowing Strategy
In: Proceedings of the 21st ACM Symposium on Principles of Programming Languages (POPL'94), 268-279
Bachmair, Leo
Ganzinger, Harald
Buchberger's algorithm: a constraint-based completion procedure
In: Proceedings of the 1st International Conference on Constraints in Computational Logics (CCL'94), 285-301
Bachmair, Leo
Ganzinger, Harald
Ordered Chaining for Total Orderings
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 435-450
Bachmair, Leo
Ganzinger, Harald
Rewrite Techniques for Transitive Relations
In: Proceedings of the 9th IEEE Symposium on Logic in Computer Science, 384-393
Barth, PeterSimplifying Clausal Satisfiability Problems
In: Proceedings of the 1st International Conference on Constraints in Computational Logics (CCL'94), 19-33
Barth, Peter
Bockmayr, Alexander
Global Consistency in CLP($\cal PB$)
In: Proceedings of the 10th Workshop Logic Programming WLP'94, 4
Basin, David A.IsaWhelk: Whelk Interpreted in Isabelle
In: Proceedings of the 11th International Conference on Logic Programming (ICLP'94), 741-741
Basin, David A.Logic Frameworks for Logic Programs
In: Proceedings of the 4th International Workshop on Logic Program Synthesis and Transformation - Meta Programming in Logic (LOPSTR'94 and META'94), 1-16
Basin, David A.
Walsh, Toby
Termination Orderings for Rippling
In: Proceedings of the 12th International Conference On Automated Deduction (CADE-12), 466-483
Bockmayr, AlexanderCutting planes in constraint logic programming (Abstract)
In: Proceedings of the 3rd International Symposium Artificial Intelligence and Mathematics,
Bockmayr, AlexanderUsing Strong Cutting Planes in Constraint Logic Programming (Extended Abstract)
In: Operations Research '93, 18th Symposium on Operations Research, 47-49
Brink, Chris
Britz, Katarina
Schmidt, Renate A.
Peirce Algebras: Extended Abstract
In: Proceedings of the 3rd International Conference on Algebraic Methodology and Software Technology (AMAST '93), 163-166
Chu, Heng
Plaisted, David A.
Semantically Guided First-Order Theorem Proving using Hyper-Linking
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 192-206
Dimopoulos, YannisClassical Methods in Nonmonotonic Reasoning
In: Proceedings of the 8th International Symposium on Methodologies for Intelligent Systems (ISMIS'94), 500-510
Dimopoulos, YannisThe Computational Value of Joint Consistency
In: Logics in Artificial Intelligence: Proceedings of the JELIA'94, 50-65
Fehrer, DetlefA Unifying Logical Framework for Reason Maintenance (Deliverable DI.1.2-3P)
In: Medlar II Report PPR2, 47-55
Fehrer, Detlef
Hustadt, Ullrich
Jaeger, Manfred
Nonnengart, Andreas
Ohlbach, Hans Jürgen
Schmidt, Renate A.
Weidenbach, Christoph
Weydert, Emil
Description Logics for Natural Language Processing
In: International Workshop on Description Logics '94, 80-84
Graf, PeterExtended Path-Indexing
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 514-528
Hanus, MichaelCombining Lazy Narrowing and Simplification
In: Proceedings of the 6th International Symposium on Programming Language Implementation and Logic Programming (PLILP'94), 370-384
Hanus, MichaelLazy Unification with Simplification
In: Proceedings of the 5th European Symposium on Programming Languages and Systems (ESOP'94), 272-286
Hanus, Michael
Zartmann, Frank
Mode Analysis of Functional Logic Programs
In: Proceedings of the 1st International Static Analysis Symposium (SAS'94), 26-42
Hustadt, UllrichA Multi-Modal Logic for Stereotyping
In: Proceedings of the 4th International Conference on User Modeling UM94, 87-92
Hustadt, UllrichCommon and Mutual Belief for Agent Modeling
In: KI-94 Workshops: Extended Abstracts, 123-124
Hustadt, UllrichCommon and Mutual Belief for Agent Modeling
In: Modeling Epistemic Propositions: Workshop during the 18th German Annual Conference on Artificial Intelligence (KI-94),
Hustadt, UllrichDo we need the closed-world assumption in knowledge representation?
In: KI-94 Workshops: Extended Abstracts, 293-294
Hustadt, UllrichDo we need the closed-world assumption in knowledge representation?
In: Working Notes of the KI'94 Workshop: Reasoning about Structured Objects: Knowledge Representation meets Databases (KRDB'94), 24-26
Jaeger, ManfredA Logic for Default Reasoning About Probabilities
In: Proceedings of the 10th Conference on Uncertainty in Artificial Intelligence (UAI'94), 352-359
Jaeger, ManfredProbabilistic Reasoning in Terminological Logics
In: Principles of Knowledge Representation an Reasoning: Proceedings of the 4th International Conference (KR94), 305-316
Johann, Patricia
Socher-Ambrosius, Rolf
Solving Simplificating Ordering Constraints
In: Proceedings of the 1st International Conference on Constraints in Computational Logics (CCL'94), 352-367
Madden, PeterFormal Methods for Automated Program Improvement
In: KI-94: Advances in Artificial Intelligence. Proceedings of the 18th German Annual Conference on Artificial Intelligence, 367-378
Nonnengart, AndreasHow to Use Modalities and Sorts in Prolog
In: Logics in Artificial Intelligence: Proceedings of the JELIA'94, 365-378
Plaisted, David A.The Search Efficiency of Theorem Proving Strategies
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 57-71
Schmidt, Renate A.Peirce Algebras and Their Applications in Artificial Intelligence and Computational Linguistics: Abstract
In: Relational Methods in Computer Science; Dagstuhl Seminar Report 80 (9403), 21-22
Schmidt, Renate A.Terminological Logics and Conceptual Graphs: An Historical Perspective
In: KI-94 Workshops: Extended Abstracts, 135-136
Socher-Ambrosius, RolfA Refined Version of General E-Unification
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 665-677
Struth, GeorgIntensionality, Possible Worlds and Propositional Attitudes: Formal and Philosophical Foundations of Modal Semantics
In: KI-94 Workshops: Extended Abstracts, 108-109
Stuber, JürgenComputing Stable Models by Program Transformation
In: Proceedings of the 11th International Conference on Logic Programming (ICLP'94), 58-73
Weidenbach, ChristophFirst-Order Tableaux with Sorts
In: TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 247-261
Weidenbach, ChristophSorts, Resolution, Tableaux and Propositional Logic
In: KI-94 Workshops: Extended Abstracts, 315-316
Werner, Andreas
Bockmayr, Alexander
Krischer, Stefan
How to realize LSE narrowing
In: Proceedings of the 4th International Conference on Algebraic and Logic Programming (ALP'94), 59-76
Weydert, EmilGeneral Belief Measures
In: Proceedings of the 10th Conference on Uncertainty in Artificial Intelligence, 575-582
Weydert, EmilHyperrational Conditionals
In: Foundations of Knowledge Representation and Reasoning, 310-332
Yoshida, Tetsuja
Bundy, Alan
Green, Ian
Walsh, Toby
Basin, David A.
Coloured Rippling: An Extension of a Theorem Proving Heuristic
In: Proceedings of the 12th European Conference on Artificial Intelligence (ECAI'94), 85-89
12
Hide details for Journal ArticleJournal Article
Bachmair, Leo
Ganzinger, Harald
Rewrite-based equational theorem proving with selection and simplification
In: Journal of Logic and Computation [4], 217-247
Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe
Refutational Theorem Proving for Hierarchic First-Order Theories
In: Applicable Algebra in Engineering, Communication and Computing (AAECC) [5], 193-212
Basin, David A.A Term Equality Problem Equivalent to Graph Isomorphism
In: Information Processing Letters [51], 61-66
Basin, David A.Generalized Rewriting in Type Theory
In: Journal of Information Processing and Cybernetics [30], 249-259
Brink, Chris
Britz, Katarina
Schmidt, Renate A.
Peirce Algebras
In: Formal Aspects of Computing [6], 339-358
Brink, Chris
Gabbay, Dov M.
Ohlbach, Hans Jürgen
Towards Automating Duality
In: Journal of Computers and Mathematics with Applications [29], 73-90
Chadha, Ritu
Plaisted, David A.
Correctness of unification without occur check in Prolog
In: Journal of Logic Programming [18], 99-122
Dimopoulos, Yannis
Magirou, Vangelis
A Graph Theoretic Approach to Default Logic
In: Information and Computation [112], 239-256
Hanus, MichaelThe Integration of Functions into Logic Programming: From Theory to Practice
In: Journal of Logic Programming [19 & 20], 583-628
Lee, Shie-Jue
Plaisted, David A.
Problem solving by searching for models with a theorem prover
In: Artificial Intelligence [69], 205-233
Lee, Shie-Jue
Plaisted, David A.
Use of replace rules in theorem proving
In: Methods of Logic in Computer Science [1], 217-240
Schmidt, Renate A.Peirce Algebras and Their Applications in Artificial Intelligence and Computational Linguistics: Abstract
In: SIGALA Newsletter [2], 27-27
2
Hide details for ReportReport
Basin, Giunchiglia, Kaufmann (ed.)Proceedings of the Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems
Struth, GeorgPhilosophical Logics: A Survey and a Bibliography
1
Hide details for Thesis - Masters thesisThesis - Masters thesis
Becker, JoachimAttachment IconEffiziente Subsumption in Deduktionssystemen
Universität des Saarlandes
1
Hide details for Thesis - Habilitation thesisThesis - Habilitation thesis
Hanus, MichaelThema der Antrittsvorlesung: Deklarative Programmierparadigmen und ihre Integration
Universität des Saarlandes
1
Hide details for Unpublished/DraftUnpublished/Draft
Ganzinger, HaraldThe Saturate System
1
Hide details for MiscellaneousMiscellaneous
Hopf, JörnGenetic Algorithms within the Framework of Evolutionary Computation
47
Hide details for 19931993
3
Hide details for Part of a BookPart of a Book
Basin, David A.
Constable, Robert L.
Metalogical Frameworks
In: Logical Environments, 1-29
Bertling, Hubert
Ganzinger, Harald
Schäfers, Renate
Nieuwenhuis, Robert
Orejas, Fernando
Completion Subsystem
In: Program Development by Specification and Transformation, The PROSPECTRA Methodology, Language Family, and System, 460-494
Matthews, Seán
Smaill, Alan
Basin, David A.
Experience with $FS_0$ as a Framework Theory
In: Logical Environments, 61-82
36
Hide details for Proceedings ArticleProceedings Article
Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe
Set Constraints are the Monadic Class
In: Eighth Annual IEEE Symposium on Logic in Computer Science, 75-83
Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe
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
Barth, PeterA Complete Symbolic 0-1 Constraint Solver
In: 3rd Workshop on Constraint Logic Programming (WCLP '93), ?
Barth, PeterLinear 0-1 Inequalities and Extended Clauses
In: Proceedings~4th International~Conference on Logic Programming and Automated Reasoning LPAR '93, 40-51
Barth, Peter
Bockmayr, Alexander
Solving 0-1 Problems in CLP($\cal PB$)
In: Proceedings 9th Conference on Artificial Intelligence for Applications (CAIA), 263-269
Basin, David A.
Bundy, Alan
Kraan, Ina
Matthews, Seán
A Framework for Program Development Based on Schematic Proof
In: Proc. 7th Intern.~Workshop on Software Specification and Design, 162-171
Basin, David A.
Matthews, Seán
A Conservative Extension of First-Order Logic and its Applications to Theorem Proving
In: Proceedings of the 13th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'93), 151-160
Basin, David A.
Walsh, Toby
Difference Unification
In: Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI-93), 116-122
Bockmayr, Alexander0-1 Constraints and 0-1 Optimization
In: 3rd Workshop on Constraint Logic Programming (WCLP '93), ?
Bockmayr, AlexanderEmbedding OR Techniques in Constraint Logic Programming
In: Operations Research '92. 17th Symposium on Operations Research, 252-254
Bockmayr, AlexanderLogic Programming with Pseudo-Boolean Constraints
In: Constraint Logic Programming---Selected Research, 327-350
Bockmayr, Alexander
Radermacher, F. J.
Künstliche Intelligenz und Operations Research
In: Grundlagen und Anwendungen der Künstlichen Intelligenz. 17. Fachtagung für Künstliche Intelligenz, 249-254
Eisinger, Norbert
Ohlbach, Hans Jürgen
Deduction Systems Based on Resolution
In: Handbook of Logic in Artificial Intelligence and Logic Programming, 184-271
Fehrer, DetlefA Unifying Framework for Reason Maintenance
In: Symbolic and Quantitative Approaches to Reasoning and Uncertainty: Proceedings European Conference ECSQARU '93, 113-120
Hanus, MichaelAnalysis of Nonlinear Constraints in CLP($\calR$)
In: Proceedings of the 10th International Conference on Logic Programming (ICLP '93), 83-99
Hanus, MichaelTowards the Global Optimization of Functional Logic Programs
In: Proc.~Workshop on Global Compilation, International Logic
Programming Symposium, 83-97
Hanus, Michael
Josephs, Berthold
A Debugging Model for Functional Logic Programs
In: Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming (PLILP-93), 28-43
Hopf, Jörn
Klawonn, Frank
Selbstlernende Fuzzy-Controller auf der Basis Genetischer Algorithmen
In: Fuzzy-Systeme '93 / Management unsicherer Informationen, 21-27
Hustadt, UllrichAbductive Disjunctive Logic Programming
In: ICLP '93 Postconference Workshop on Abductive Reasoning, ?
Hustadt, UllrichAutomated Support for the Development of Non-classical Logics
In: Workshop: Modellierung epistemischer Propositionen, KI '93,
Hustadt, Ullrich
Nonnengart, Andreas
Modalities in Knowledge Representation
In: Proc. of the 6th Australian Joint Conference on Artificial Intelligence (AI '93), 249-254
Kraan, Ina
Basin, David A.
Bundy, Alan
Logic Program Synthesis via Proof Planning
In: International Workshop on Logic Program Synthesis and Transformation (LOPSTR '92), 1-14
Kraan, Ina
Basin, David A.
Bundy, Alan
Middle-Out Reasoning for Logic Program Synthesis
In: Proc.~10th Intern. Conference on Logic Programing (ICLP '93), 441-455
Madden, Peter
Bundy, Alan
General Proof Theoretic Techniques for Automatic
Programing
In: Proceedings of the EAST-WEST AI CONFERENCE: From
Theory to Practice - EWAIC'93,
Nonnengart, AndreasFirst-Order Modal Logic Theorem Proving and Functional Simulation
In: Proc.~13th Intern.~Joint Conference on Artificial Intelligence (IJCAI '93), 80-85
Ohlbach, Hans JürgenEin kurzes Tutorial über funktionale Übersetzung von Modallogik nach Prädikatenlogik
In: Bericht Nr. 15/93: Recommendations for Extensions to BGP-MS, 19-26
Ohlbach, Hans JürgenOptimized Translation of Multi Modal Logic into Predicate Logic
In: Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning (LPAR'93), 253-264
Plaisted, David A.Equational Reasoning and Term Rewriting Systems
In: Handbook of Logic in Artificial Intelligence and Logic Programming, 273-364
Schmidt, Renate A.Terminological Representation, Natural Language \& Relation Algebra
In: GWAI-92: Advances in Artificial Intelligence: Proc.~16th German Workshop on Artificial Intelligence, 357-371
Socher-Ambrosius, RolfUnification in Order-Sorted Logic with Term Declarations
In: Proceedings of the 4th Conference on Logic Programming and Automated Reasoning (LPAR-93), 301-308
Weidenbach, ChristophA New Sorted Logic
In: GWAI-92: Advances in Artificial Inteligence, Proceedings 16th German Workshop on Artificial Intelligence, 43-54
Weidenbach, ChristophExtending the Resolution Method with Sorts
In: Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI '93), 60-65
Werner, Andreas
Bockmayr, Alexander
Krischer, Stefan
A Concept for the Implementation of LSE Narrowing
In: 9.~Workshop Logische Programmierung, ?
Werner, Andreas
Bockmayr, Alexander
Krischer, Stefan
How to Realize LSE Narrowing
In: Proceedings of the 2nd International Workshop on Functional/Logic Programming, ?-?
Weydert, EmilDefault Quantifiers: About Plausible Reasoning in First-Order Contexts
In: Working Notes of the Dutch/German Workshop on Nonmonotonic Reasoning Techniques and their Applications, ?
Weydert, EmilPlausible Inference for Default Conditionals
In: Symbolic and Quantitative Approaches to Reasoning and Uncertainty: Proceedings of the European Conference ECSQARU '93, 356-363
6
Hide details for Journal ArticleJournal Article
Barnett, Richard
Basin, David A.
Hesketh, Jane
A Recursion Planning Analysis of Inductive Completion
In: Annals of Mathematics and Artificial Intelligence [8], 363-381
Bockmayr, AlexanderConditional Narrowing Modulo a Set of Equations
In: Applicable Algebra in Engineering, Communication and Computing [4], 147-168
Chadha, Ritu
Plaisted, David A.
On the mechanical derivation of loop invariants
In: Journal of Symbolic Computation [15], 705-744
Dimopoulos, Yannis
Magirou, Vangelis
Papadimitriou, Christos
On Kernels, Defaults and Even Graphs
In: Annals of Mathematics and Artificial Intelligence,
Jaeger, ManfredCircumscription: Completeness Reviewed
In: Artificial Intelligence [60], 293-301
Ohlbach, Hans JürgenTranslation Methods for Non-Classical Logics: An Overview
In: Bulletin of the Interest Group in Propositional and Predicate Logics (IGPL) [1], 69-90
1
Hide details for ReportReport
Werner, Andreas
Bockmayr, Alexander
Krischer, Stefan
How to Realize LSE Narrowing
1
Hide details for Thesis - Habilitation thesisThesis - Habilitation thesis
Ohlbach, Hans JürgenThema der Antrittsvorlesung: Transformation logischer Systeme
Universität des Saarlandes
26
Hide details for 19921992
4
Hide details for Part of a BookPart of a Book
Eisinger, Norbert
Nonnengart, Andreas
Präcklein, Axel
Termersetzungssysteme
In: Deduktionssysteme -- Automatisierung des logischen Denkens, 126-149
Ganzinger, Harald
Stuber, Jürgen
Inductive theorem proving by consistency for first-order clauses
In: Informatik - Festschrift zum 60. Geburtstag von Günter Hotz, 441-462
Hanus, MichaelLogic Programming with Type Specifications
In: Types in Logic Programming, 91-140
Nonnengart, Andreas
Ohlbach, Hans Jürgen
Modal- und Temporallogik
In: Deduktionssysteme - Automatisierung des logischen Denkens, 239-284
17
Hide details for Proceedings ArticleProceedings Article
Bachmair, Leo
Ganzinger, Harald
Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria
In: Logic Programming and Automated Reasoning, 273-284
Bachmair, Leo
Ganzinger, Harald
Lynch, Christopher
Snyder, Wayne
Basic Paramodulation and Superposition
In: Proceedings of the 11th International Conference on Automated Deduction (CADE-11), 462-476
Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe
Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434
Basin, David A.
Walsh, Toby
Difference Matching
In: Proceedings of the11th International Conference on Automated Deduction (CADE-11), 295-309
Bockmayr, AlexanderA Theoretical Basis for Constraint Logic and Functional Programming
In: Proc.~1st African Conference on Research in Computer Science, 793-804
Bockmayr, AlexanderAlgebraic and Logical Aspects of Unification
In: Proc.~1st Workshop on Word Equations and Related Topics, 171-180
Bockmayr, AlexanderModel-Theoretic Aspects of Unification
In: Proceedings of the 1st Workshop on Word Equations and Related Topics, 181-196
Frank, Ian
Basin, David A.
Bundy, Alan
Finesse: An Adaptation of Proof-Planning to Declarer Play in Bridge
In: Proceedings of the 10th European Conference on Artificial Intelligence (ECAI-92), 72-76
Gabbay, Dov M.
Ohlbach, Hans Jürgen
From a Hilbert Calculus to its Model Theoretic Semantics
In: Proc.~4th Annual UK Conference on Logic Programming (APULK '92), 218-252
Gabbay, Dov M.
Ohlbach, Hans Jürgen
Quantifier Elimination in Second-Order Predicate Logic
In: Principles of Knowledge Representation and Reasoning (KR92),, 425-435
In: South African Computer Journal [7], 425-435
Ganzinger, Harald
Waldmann, Uwe
Termination Proofs of Well-Moded Logic Programs Via Conditional Rewrite Systems
In: Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems '92, 430-437
Hanus, MichaelImproving Control of Logic Programs by Using Functional Logic Languages
In: Proceedings 4th International Symposium on Programming Language Implementation and Logic Programming, 1-23
Hanus, MichaelIncremental Rewriting in Narrowing Derivations
In: Proceedings of the 3rd International Conference on Algebraic and Logic Programming (ALP-92), 228-243
Hanus, MichaelOn the Completeness of Residuation
In: Proceedings of the 1992 Joint International Conference and Symposium on Logic Programming, 192-206
Madden, PeterAutomated Program Transformation Through Proof Transformation
In: Proceedings of the 11th International Conference on Automated Deduction (CADE-11), 446-460
Matthews, SeánReflection in a Logical System
In: Proc.~IMSA '92 Workshop on Reflection and Meta-Level Architecture, 178-183
Socher-Ambrosius, RolfA Goal Oriented Strategy Based on Completion
In: Proc.~3rd Intern.~Conference on Algebraic and Logic Programming, 435-445
4
Hide details for Journal ArticleJournal Article
Gabbay, Dov M.
Ohlbach, Hans Jürgen
Quantifier Elimination in Second-Order Predicate Logic
In: South African Computer Journal [7], 35-43
Ohlbach, Hans JürgenLogic Engineering: Konstruktion von Logiken
In: KI [3], 34-38
Socher-Ambrosius, RolfHow to Avoid the Derivation of Redundant Clauses in Reasoning Systems
In: Journal of Automated Reasoning [9], 325-336
Waldmann, UweSemantics of Order-Sorted Specifications
In: Theoretical Computer Science [94], 1-35
1
Hide details for Thesis - Masters thesisThesis - Masters thesis
Graf, PeterUnification Using Dynamic Sorts
Universität des Saarlandes
26
Hide details for 19911991
13
Hide details for Proceedings ArticleProceedings Article
Bachmair, Leo
Ganzinger, Harald
Completion of first-order clauses with equality by strict superposition
In: Proceedings of the 2nd International Workshop on Conditional and Typed Rewriting, 162-180
Bachmair, Leo
Ganzinger, Harald
Perfect model semantics for logic programs with equality
In: Proceedings International Conference on Logic Programming '91, 645-659
Basin, David A.
Giunchiglia, Fausto
Traverso, P.
Automating Meta-Theory Creation and System Extension
In: Proc. Trends in AI: 2nd Congress of the Italian Association for Artificial Intelligence (AI*IA), 48-57
Basin, David A.
Howe, D.
Some Normalization Properties of Martin-Löf's Type Theory, and Applications
In: International Conference on Theoretical Aspects of Computer Software (TACS '91), 475-494
Basin, David A.
Kaufmann, Matt
The Boyer-Moore Prover and Nuprl: An Experimental Comparison
In: Logical Frameworks, 90-119
Baumeister, HubertUnifying Initial and Loose Semantics of Parameterized Specifications in an Arbitrary Institution
In: Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT '91), 103-120
Cunningham, J.
Gabbay, Dov M.
Ohlbach, Hans Jürgen
Towards the MEDLAR Framework
In: ESPRIT '91 Conference Proceedings, 822-841
Hanus, MichaelEfficient Implementation of Narrowing and Rewriting
In: Proc. Intern. Workshop on Processing Declarative Knowledge, 344-365
Hanus, MichaelParametric Order-Sorted Types in Logic Programming
In: Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT-91), 181-200
Krischer, Stefan
Bockmayr, Alexander
Detecting Redundant Narrowing Derivations by the LSE-SL Reducibility Test
In: Proceedings of the 4th International Conference on Rewriting Techniques and Applications (RTA '91), 74-85
Ohlbach, Hans Jürgen
Herzig, A.
Parameter Structures for Parametrized Modal Operators
In: Proc.~Intern.~Joint Conference on Artificial Intelligence (IJCAI'91), 512-517
Ohlbach, Hans Jürgen
Siekmann, Jörg H.
The Markgraf Karl Refutation Procedure
In: Computational Logic, Essays in Honor of Alan Robinson, 41-112
Socher-Ambrosius, RolfBoolean Algebra Admits no Convergent Term Rewriting System
In: Proceedings of the 4th International Conference on Rewriting Techniques and Applications (RTA-91), 264-274
10
Hide details for Journal ArticleJournal Article
Basin, David A.
Brown, G. M.
Leeser, M. E.
Formally Verified Synthesis of Combinational CMOS Circuits
In: Integration: The Intern. Journal of VLSI Design [11], 235-250
Bockmayr, Alexander
Brzoska, C.
Deussen, P.
Varsek, I.
KA-Prolog: Erweiterungen einer logischen Programmiersprache und ihre effiziente Implementierung
In: Informatik--Forschung und Entwicklung [6], 128-140
Brink, Chris
Rewitzky, I. M.
Schmidt, Renate A.
Autodescriptivity: Beware!
In: The Computer Journal [34], 380-381
Eisinger, Norbert
Ohlbach, Hans Jürgen
Präcklein, Axel
Reduction Rules for Resolution Based Systems
In: Artificial Intelligence [50], 141-181
Ganzinger, HaraldA completion procedure for conditional equations
In: Journal of Symbolic Computation [11], 51-81
Ganzinger, HaraldOrder-Sorted Completion: The Many-Sorted Way
In: Theoretical Computer Science [89], 3-32
Hanus, MichaelHorn Clause Programs with Polymorphic Types: Semantics and Resolution
In: Theoretical Computer Science [89], 63-106
Ohlbach, Hans JürgenSemantics Based Translation Methods for Modal Logics
In: Journal of Logic and Computation [1], 691-746
Socher-Ambrosius, RolfOn the Relation Between Completion Based and Resolution Based Theorem Proving
In: Journal of Symbolic Computation [11], 129-148
Socher-Ambrosius, RolfOptimizing the Clausal Normal Form Transformation
In: Journal of Automated Reasoning [7], 325-336
1
Hide details for ReportReport
Socher-Ambrosius, RolfOn the Church-Rosser Property in Left-Linear Systems
2
Hide details for Thesis - Masters thesisThesis - Masters thesis
Reinold, MichaelTransformation in dichten Wäldern
Universität des Saarlandes
Stuber, JürgenAttachment IconInductive Theorem Proving for Horn Clauses
Universität Dortmund
2
Hide details for 19901990
1
Hide details for Journal ArticleJournal Article
Brahm, Uwe
Pitz, Werner
Parkwächter
In: c't Magazin für computer technik [-], 252-253
1
Hide details for Thesis - Masters thesisThesis - Masters thesis
Baumeister, HubertAttachment IconÜber die Stabilität parameterisierter algebraischer Spezifikationen
Universität Dortmund
1
Hide details for 19881988
1
Hide details for Thesis - PhD thesisThesis - PhD thesis
Ohlbach, Hans JürgenA Resolution Calculus for Modal Logics
Universität Kaiserslautern
782

Previous Page | Next Page | Expand All | Collapse All | Search (Full Text)