| # |  | Year | Author(s) [non member] | | Title | Type | |
|---|
| 1 |
 | Baader, Franz |
| |
| | 1995 | Baader, Franz
Ohlbach, Hans Jürgen | | A Multi-Dimensional Terminological Knowledge Representation Language
In: Journal of Applied Non-Classical Logics [5], 153-198 | Journal Article | |
| 9 |
| Baader, Franz (ed.) |
| |
| | 2003 | 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 | Proceedings Article | |
| | 2003 | Korovin, Konstantin
[Voronkov, Andrei] |  | AC-compatible Knuth-Bendix Order
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 47-59 | Proceedings Article | |
| | 2003 | Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe | | Superposition modulo a Shostak Theory
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 182-196 | Proceedings Article | |
| | 2003 | Ganzinger, Harald
[Stuber, Jürgen] | | Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 335-349 | Proceedings Article | |
| | 2003 | [Gaillourdet, Jean-Marie]
Hillenbrand, Thomas
[Löchner, Bernd]
[Spies, Hendrik] | | The New WALDMEISTER Loop at Work
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 317-321 | Proceedings Article | |
| | 2003 | de Nivelle, Hans | | Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 365-379 | Proceedings Article | |
| | 1996 | 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 | Part of a Book | |
| | 1994 | 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 | Proceedings Article | |
| | 1994 | Hustadt, Ullrich | | Do 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 | Proceedings Article | |
| 1 |
| Bachem, A. (ed.) |
| |
| | 1994 | Bockmayr, Alexander | | Using Strong Cutting Planes in Constraint Logic Programming (Extended Abstract)
In: Operations Research '93, 18th Symposium on Operations Research, 47-49 | Proceedings Article | |
| 20 |
| Bachmair, Leo |
| |
| | 2001 | Bachmair, Leo
Ganzinger, Harald | | Resolution Theorem Proving
In: Handbook of Automated Reasoning, 19-99 | Part of a Book | |
| | 1998 | 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 | Proceedings Article | |
| | 1998 | Bachmair, Leo
Ganzinger, Harald | | Equational Reasoning in Saturation-Based Theorem Proving
In: Automated Deduction: A Basis for Applications, 353-397 | Part of a Book | |
| | 1998 | [Bachmair, Leo]
Ganzinger, Harald | | Ordered Chaining Calculi for First-Order Theories of Transitive Relations
In: Journal of the ACM [45], 1007-1049 | Journal Article | |
| | 1998 | Bachmair, Leo
Ganzinger, Harald | | Strict Basic Superposition
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 160-174 | Proceedings Article | |
| | 1995 | Bachmair, Leo
Ganzinger, Harald | | Associative-Commutative Superposition
In: Proceedings of the 4th International Workshop on Conditional and Typed Rewrite Systems (CTRS-94), 1-14 | Proceedings Article | |
| | 1995 | Bachmair, Leo
Ganzinger, Harald
[Lynch, Christopher]
[Snyder, Wayne] | | Basic Paramodulation
In: Information and Computation [121], 172-192 | Journal Article | |
| | 1995 | 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 | Proceedings Article | |
| | 1994 | 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 | Proceedings Article | |
| | 1994 | Bachmair, Leo
Ganzinger, Harald | | Ordered Chaining for Total Orderings
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 435-450 | Proceedings Article | |
| | 1994 | 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 | Journal Article | |
| | 1994 | Bachmair, Leo
Ganzinger, Harald | | Rewrite-based equational theorem proving with selection and simplification
In: Journal of Logic and Computation [4], 217-247 | Journal Article | |
| | 1994 | Bachmair, Leo
Ganzinger, Harald | | Rewrite Techniques for Transitive Relations
In: Proceedings of the 9th IEEE Symposium on Logic in Computer Science, 384-393 | Proceedings Article | |
| | 1993 | [Bachmair, Leo]
Ganzinger, Harald
Waldmann, Uwe | | Set Constraints are the Monadic Class
In: Eighth Annual IEEE Symposium on Logic in Computer Science, 75-83 | Proceedings Article | |
| | 1993 | [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 | Proceedings Article | |
| | 1992 | 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 | Proceedings Article | |
| | 1992 | Bachmair, Leo
Ganzinger, Harald | | Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria
In: Logic Programming and Automated Reasoning, 273-284 | Proceedings Article | |
| | 1992 | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | | Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434 | Proceedings Article | |
| | 1991 | 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 | Proceedings Article | |
| | 1991 | Bachmair, Leo
Ganzinger, Harald | | Perfect model semantics for logic programs with equality
In: Proceedings International Conference on Logic Programming '91, 645-659 | Proceedings Article | |
| 1 |
| |
| | 2000 | Stuber, Jürgen | | Deriving Theory Superposition Calculi from Convergent Term Rewriting Systems
In: Proceedings of the 11th International Conference Rewriting Techniques and Applications (RTA-00), 229-245 | Proceedings Article | |
| 1 |
| |
| | 1996 | Bach, Alexander | | Static analysis of functional programs via Linear Logic
Universität des Saarlandes | Thesis - Masters thesis | |
| 3 |
| |
| | 2005 | Backes, Werner | | Programmanalyse des XRTL Zwischencodes
Universität des Saarlandes | Thesis - PhD thesis | |
| | 2001 | Backes, Werner
[Wetzel, Susanne] | | Lattice Basis Reduction with Dynamic Approximation
In: Proceedings of the 4th Workshop On Algorithm Engineering (WAE-2000), 63-73 | Proceedings Article | |
| | 2000 | 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 | Proceedings Article | |
| 3 |
| |
| | 1993 | Basin, David A.
Walsh, Toby | | Difference Unification
In: Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI-93), 116-122 | Proceedings Article | |
| | 1993 | Weidenbach, Christoph | | Extending the Resolution Method with Sorts
In: Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI '93), 60-65 | Proceedings Article | |
| | 1993 | Nonnengart, Andreas | | First-Order Modal Logic Theorem Proving and Functional Simulation
In: Proc.~13th Intern.~Joint Conference on Artificial Intelligence (IJCAI '93), 80-85 | Proceedings Article | |
| 1 |
| |
| | 2003 | [Schmidt, Renate A.]
[Tishkovsky, Dmitry] | | Combining Dynamic Logic and Doxastic Modal Logics
In: Advances in Modal Logic, 371-391 | Part of a Book | |
| 1 |
| |
| | 2001 | [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 | Proceedings Article | |
| 1 |
| |
| | 2006 | Cook, Byron
Podelski, Andreas
Rybalchenko, Andrey | | Terminator: Beyond Safety
In: Computer aided verification : 18th International Conference, CAV 2006, 415-418 | Proceedings Article | |
| 2 |
| |
| | 2003 | 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 | Journal Article | |
| | 2002 | 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 | Proceedings Article | |
| 1 |
| Baral, C. (ed.) |
| |
| | 2000 | Booth, Richard | | The lexicographic closure as a revision process
In: Proceedings of the 8th International Workshop on Non-Monotonic Reasoning (NMR 2000), ? | Electronic Proceedings Article | |
| 2 |
| Barkaoui, Kamel (ed.) |
| |
| | 2006 | [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 | Proceedings Article | |
| | 2006 | 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 | Proceedings Article | |
| 1 |
| |
| | 1993 | Barnett, Richard
Basin, David A.
Hesketh, Jane | | A Recursion Planning Analysis of Inductive Completion
In: Annals of Mathematics and Artificial Intelligence [8], 363-381 | Journal Article | |
| 1 |
| |
| | 2005 | 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 | Proceedings Article | |
| 14 |
| |
| | 1998 | [Barth, Peter]
Bockmayr, Alexander | | Modelling Discrete Optimisation Problems in Constraint Logic Programming
In: Annals of Operations Research [81], 467-496 | Journal Article | |
| | 1997 | Barth, Peter
Bockmayr, Alexander | | PLAM: ProLog and Algebraic Modelling
In: Proceedings of the 5th International Conference on the Practical Application of Prolog, 73-82 | Proceedings Article | |
| | 1996 | Bockmayr, Alexander
Barth, Peter
Kasper, Thomas | | Methods and Tools for Pseudo-Boolean Problems
In: 2. Workshop Boolesche Probleme, 105-109 | Proceedings Article | |
| | 1996 | 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 | Proceedings Article | |
| | 1995 | 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 | Proceedings Article | |
| | 1995 | Barth, Peter | | Logic-based 0-1 constraint programming | Book | |
| | 1995 | Barth, Peter | | Logic-based 0-1 Constraint Solving in Constraint Logic Programming
Fachbereich Informatik, Universität des Saarlandes, Germany | Thesis - PhD thesis | |
| | 1995 | Barth, Peter
Bockmayr, Alexander | | Pseudo-Boolean Constraint Logic Programming
In: Computational Logic. The Newsletter of the European Network in Computational Logic [2], 52-53 | Journal Article | |
| | 1995 | Barth, Peter
[Kleine Büning, Hans]
Weidenbach, Christoph | | Workshop CPL Computational Propositional Logic
In: KI-95 Activities: Workshops, Posters, Demos, 71-72 | Proceedings Article | |
| | 1994 | Barth, Peter
Bockmayr, Alexander | | Global Consistency in CLP($\cal PB$)
In: Proceedings of the 10th Workshop Logic Programming WLP'94, 4 | Proceedings Article | |
| | 1994 | Barth, Peter | | Simplifying Clausal Satisfiability Problems
In: Proceedings of the 1st International Conference on Constraints in Computational Logics (CCL'94), 19-33 | Proceedings Article | |
| | 1993 | Barth, Peter | | A Complete Symbolic 0-1 Constraint Solver
In: 3rd Workshop on Constraint Logic Programming (WCLP '93), ? | Proceedings Article | |
| | 1993 | Barth, Peter | | Linear 0-1 Inequalities and Extended Clauses
In: Proceedings~4th International~Conference on Logic Programming and Automated Reasoning LPAR '93, 40-51 | Proceedings Article | |
| | 1993 | Barth, Peter
Bockmayr, Alexander | | Solving 0-1 Problems in CLP($\cal PB$)
In: Proceedings 9th Conference on Artificial Intelligence for Applications (CAIA), 263-269 | Proceedings Article | |
| 54 |
| Basin, David A. |
| |
| | 2002 | Basin, David A.
Matthews, Sean | | Logical Frameworks
In: Handbook of Philosophical Logic, 89-164 | Part of a Book | |
| | 2001 | [Ayari, Abdelwaheb]
Basin, David A. | | A Higher-order Interpretation of Deductive Tableau
In: Journal of Symbolic Computation [31], 487-520 | Journal Article | |
| | 2001 | [Basin, David A.]
Ganzinger, Harald | | Automated Complexity Analysis Based on Ordered Resolution
In: Journal of the ACM [48], 70-109 | Journal Article | |
| | 2000 | [Anderson, Penny]
Basin, David A. | | Program Development Schemata as Derived Rules
In: Journal of Symbolic Computation [30], 5-36 | Journal Article | |
| | 2000 | Matthews, Seán
[Basin, David A.] | | Structuring Metatheory on Inductive Definitions
In: Information and Computation [162], 80-95 | Journal Article | |
| | 1999 | Basin, David A.
Krieg-Brückner, Bernd | | Formalization of the Development Process
In: Algebraic foundations of systems specification, 521-562 | Part of a Book | |
| | 1999 | Basin, David A.
Friedrich, Stefan | | Modeling a Hardware Synthesis Methodology in Isabelle
In: Formal Methods in Systems Design [15], 99-122 | Journal Article | |
| | 1998 | [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 | Proceedings Article | |
| | 1998 | Basin, David A.
[Klarlund, Nils] | | Automata Based Symbolic Reasoning in Hardware Verification
In: Formal Methods in Systems Design [13], 255-288 | Journal Article | |
| | 1998 | [Basin, David A.]
Matthews, Seán
[Viganò, Luca] | | Labelled Modal Logics: quantifiers
In: Journal of Logic, Language and Information [7], 237-263 | Journal Article | |
| | 1998 | [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 | Proceedings Article | |
| | 1998 | Basin, David A.
Matthews, Seán
Viganò, Luca | | Natural Deduction for Non-Classical Logics
In: Studia Logica [60], 119-160 | Journal Article | |
| | 1998 | Matthews, Seán
Basin, David A. | | Scoped Metatheorems
In: Electronic Notes in Computer Science [15], 1-14 | Journal Article | |
| | 1998 | [Frank, Ian]
Basin, David A. | | Search in Games with Incomplete Information: A Case Study Using Bridge Card Play
In: Artificial Intelligence [100], 87-123 | Journal Article | |
| | 1997 | 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 | Proceedings Article | |
| | 1997 | Basin, David A.
Matthews, Seán
Viganò, Luca | | Labelled Propositional Modal Logics: Theory and Practice
In: Journal of Logic and Computation [7], 685-717 | Journal Article | |
| | 1997 | 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 | Proceedings Article | |
| | 1996 | Basin, David A.
[Walsh, Toby] | | A Calculus for and Termination of Rippling
In: Automated mathematical induction, 147-180 | Part of a Book | |
| | 1996 | Basin, David A.
[Walsh, Toby] | | A Calculus for and Termination of Rippling
In: Journal of Automated Reasoning [16], 147-180 | Journal Article | |
| | 1996 | 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 | Part of a Book | |
| | 1996 | Basin, David A.
Matthews, Seán | | Adding Metatheoretic facilities to First-order Theories
In: Journal of Logic and Computation [6], 835-849 | Journal Article | |
| | 1996 | 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 | Proceedings Article | |
| | 1996 | [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 | Proceedings Article | |
| | 1996 | 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 | Proceedings Article | |
| | 1996 | 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 | Proceedings Article | |
| | 1996 | [Kraan, Ina]
Basin, David A.
[Bundy, Alan] | | Middle-Out Reasoning for Synthesis and Induction
In: Automated mathematical induction, 113-145 | Part of a Book | |
| | 1996 | [Kraan, Ina]
Basin, David A.
[Bundy, Alan] | | Middle-out reasoning for synthesis and induction
In: Journal of Automated Reasoning [16], 113-145 | Journal Article | |
| | 1996 | 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 | Proceedings Article | |
| | 1996 | [Frank, Ian]
Basin, David A. | | Search in Games with Incomplete Information: A Case Study Using Bridge Card Play | Report | |
| | 1996 | 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 | Proceedings Article | |
| | 1995 | Anderson, Penny
Basin, David A. | | Deriving and Applying Logic Program Transformers
In: Algorithms, Concurrency and Knowledge (1995 Asian Computing Science Conference), 301-318 | Proceedings Article | |
| | 1995 | 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 | Proceedings Article | |
| | 1995 | Ayari, Abdelwaheb
Basin, David A. | | Interpretation of the Deductive Tableau in HOL
In: Proceedings of the First Isabelle Users Workshop, 91-100 | Proceedings Article | |
| | 1995 | Basin, David A. | | Thema der Antrittsvorlesung: MONA - Ein Werkzeug zur Systemverifikation und -entwicklung
Universität des Saarlandes | Thesis - Habilitation thesis | |
| | 1994 | Basin, David A. | | A Term Equality Problem Equivalent to Graph Isomorphism
In: Information Processing Letters [51], 61-66 | Journal Article | |
| | 1994 | [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 | Proceedings Article | |
| | 1994 | Basin, David A. | | Generalized Rewriting in Type Theory
In: Journal of Information Processing and Cybernetics [30], 249-259 | Journal Article | |
| | 1994 | Basin, David A. | | IsaWhelk: Whelk Interpreted in Isabelle
In: Proceedings of the 11th International Conference on Logic Programming (ICLP'94), 741-741 | Proceedings Article | |
| | 1994 | 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 | Proceedings Article | |
| | 1994 | Basin, David A.
[Walsh, Toby] | | Termination Orderings for Rippling
In: Proceedings of the 12th International Conference On Automated Deduction (CADE-12), 466-483 | Proceedings Article | |
| | 1993 | 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 | Proceedings Article | |
| | 1993 | 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 | Proceedings Article | |
| | 1993 | Barnett, Richard
Basin, David A.
Hesketh, Jane | | A Recursion Planning Analysis of Inductive Completion
In: Annals of Mathematics and Artificial Intelligence [8], 363-381 | Journal Article | |
| | 1993 | Basin, David A.
Walsh, Toby | | Difference Unification
In: Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI-93), 116-122 | Proceedings Article | |
| | 1993 | Matthews, Seán
Smaill, Alan
Basin, David A. | | Experience with $FS_0$ as a Framework Theory
In: Logical Environments, 61-82 | Part of a Book | |
| | 1993 | 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 | Proceedings Article | |
| | 1993 | Basin, David A.
Constable, Robert L. | | Metalogical Frameworks
In: Logical Environments, 1-29 | Part of a Book | |
| | 1993 | 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 | Proceedings Article | |
| | 1992 | Basin, David A.
Walsh, Toby | | Difference Matching
In: Proceedings of the11th International Conference on Automated Deduction (CADE-11), 295-309 | Proceedings Article | |
| | 1992 | 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 | Proceedings Article | |
| | 1991 | 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 | Proceedings Article | |
| | 1991 | 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 | Journal Article | |
| | 1991 | 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 | Proceedings Article | |
| | 1991 | Basin, David A.
Kaufmann, Matt | | The Boyer-Moore Prover and Nuprl: An Experimental Comparison
In: Logical Frameworks, 90-119 | Proceedings Article | |
| 1 |
| |
| | 1994 | | | Proceedings of the Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems | Report | |
| 2 |
| |
| | 2004 | 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 | Proceedings Article | |
| | 2004 | 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 | Proceedings Article | |
| 4 |
| Baumeister, Hubert |
| |
| | 1999 | Baumeister, Hubert | | Relations between Abstract Datatypes modeled as Abstract Datatypes
Universität des Saarlandes | Thesis - PhD thesis | |
| | 1995 | Baumeister, Hubert | | Relations 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 | Proceedings Article | |
| | 1991 | Baumeister, Hubert | | Unifying 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 | Proceedings Article | |
| | 1990 | Baumeister, Hubert | | Über die Stabilität parameterisierter algebraischer Spezifikationen
Universität Dortmund | Thesis - Masters thesis | |
| 13 |
| |
| | 2006 | 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 | Electronic Proceedings Article | |
| | 2006 | Baumgartner, Peter
Fuchs, Alexander
[Tinelli, Cesare] | | Implementing the Model Evolution Calculus
In: International Journal on Artificial Intelligence Tools [15], 21-52 | Journal Article | |
| | 2005 | Baumgartner, Peter
[Furbach, Ulrich]
[Yahya, Adnan] | | Automated Reasoning, Knowledge Representation and Management
In: KI - Künstliche Intelligenz [1], 5-11 | Journal Article | |
| | 2005 | 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 | Part of a Book | |
| | 2005 | Baumgartner, Peter
Suchanek, Fabian | | Model-Generation Theorem Proving for First-Order Logic Ontologies | Unpublished/Draft | |
| | 2005 | 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 | Proceedings Article | |
| | 2005 | Baumgartner, Peter
[Tinelli, Cesare] | | The Model Evolution Calculus with Equality
In: Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 392-408 | Proceedings Article | |
| | 2004 | 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 | Proceedings Article | |
| | 2004 | 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 | Proceedings Article | |
| | 2004 | Baumgartner, Peter
[Grabowski, Barbara]
[Oevel, Walter]
[Melis, Erica] | | In2Math - Interaktive Mathematik- und Informatikgrundausbildung
In: Softwaretechnik-Trends [24], 36-45 | Journal Article | |
| | 2004 | Baumgartner, Peter
[Furbach, Ulrich]
[Gross-Hardt, Margret]
[Sinner, Alex] | | Living Book -- Deduction, Slicing, and Interaction
In: Journal of Automated Reasoning [32], 259-286 | Journal Article | |
| | 2004 | Baumgartner, Peter
[Burchardt, Aljoscha] | | Logic Programming Infrastructure for Inferences on FrameNet
In: Logics in artificial intelligence : 9th European Conference, JELIA 2004, 591-603 | Proceedings Article | |
| | 2004 | 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 | Proceedings Article | |
| 3 |
| |
| | 2006 | 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 | Electronic Proceedings Article | |
| | 2006 | | | IJCAR'06 Workshop : Disproving'06: Non-Theorems, Non-Validity, Non-Provability | Electronic Proceedings | |
| | 2006 | Hillenbrand, Thomas
Topic, Dalibor
Weidenbach, Christoph | | Sudokus as Logical Puzzles
In: Proceedings of the Third Workshop on Disproving, 2-12 | Electronic Proceedings Article | |
| 3 |
| |
| | 2005 | Jacobs, Swen
Waldmann, Uwe | | Comparing Instance Generation Methods for Automated Reasoning
In: Automated reasoning with analytic tableaux and related methods : International Conference, TABLEAUX 2005, 153-168 | Proceedings Article | |
| | 2005 | [Georgieva, Lilia]
Maier, Patrick | | Description Logics for Shape Analysis
In: Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 321-330 | Proceedings Article | |
| | 2005 | 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 | Proceedings Article | |
| 1 |
| |
| | 1994 | Becker, Joachim | | Effiziente Subsumption in Deduktionssystemen
Universität des Saarlandes | Thesis - Masters thesis | |
| 1 |
| |
| | 2006 | [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 | Proceedings Article | |
| 1 |
| |
| | 1993 | Werner, Andreas
Bockmayr, Alexander
Krischer, Stefan | | A Concept for the Implementation of LSE Narrowing
In: 9.~Workshop Logische Programmierung, ? | Proceedings Article | |
| 1 |
| |
| | 2007 | [Podelski, Andreas]
Wagner, Silke | | A Sound and Complete Proof Rule for Region Stability of Hybrid Systems
In: Hybrid systems: computation and control : 10th International Conference, HSCC 2007, 750-753 | Poster | |
| 1 |
| |
| | 2007 | [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 | Journal Article | |
| 1 |
| |
| | 2001 | Weydert, Emil | | Rankings 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 | Proceedings Article | |
| 3 |
| |
| | 1993 | Bockmayr, Alexander | | 0-1 Constraints and 0-1 Optimization
In: 3rd Workshop on Constraint Logic Programming (WCLP '93), ? | Proceedings Article | |
| | 1993 | Barth, Peter | | A Complete Symbolic 0-1 Constraint Solver
In: 3rd Workshop on Constraint Logic Programming (WCLP '93), ? | Proceedings Article | |
| | 1993 | Bockmayr, Alexander | | Logic Programming with Pseudo-Boolean Constraints
In: Constraint Logic Programming---Selected Research, 327-350 | Proceedings Article | |
| 2 |
| |
| | 2004 | [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 | Proceedings Article | |
| | 2004 | 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 | Proceedings Article | |
| 1 |
| Bertling, Hubert |
| |
| | 1993 | 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 | Part of a Book | |
| 2 |
| Besnard, Philippe (ed.) |
| |
| | 2001 | Weydert, Emil | | Rankings 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 | Proceedings Article | |
| | 1995 | Weydert, Emil | | Defaults and Infinitesimals. Defeasible inference by nonarchimedean entropy maximization
In: Proceedings of the 11th Conference on Uncertainty in Artificial Intelligence (UAI 95), 540-547 | Proceedings Article | |
| 2 |
| |
| | 2007 | [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 | Proceedings Article | |
| | 2007 | [Beyer, Dirk]
[Henzinger, Thomas]
[Majumdar, Rupak]
Rybalchenko, Andrey | | Path Invariants
In: PLDI'07 : Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 300-309 | Proceedings Article | |
| 2 |
| Bezem, Marc |
| |
| | 2002 | [Bezem, Marc]
[Hendriks, Dimitri]
de Nivelle, Hans | | Automated Proof Construction in Type Theory using Resolution
In: Journal of Automated Reasoning [29], 253-275 | Journal Article | |
| | 2000 | 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 | Proceedings Article | |
| 3 |
| |
| | 1998 | Bachmair, Leo
Ganzinger, Harald | | Equational Reasoning in Saturation-Based Theorem Proving
In: Automated Deduction: A Basis for Applications, 353-397 | Part of a Book | |
| | 1998 | Weidenbach, Christoph | | Sorted Unification and Tree Automata
In: Automated Deduction - A Basis for Applications, 291-320 | Part of a Book | |
| | 1998 | Stuber, Jürgen | | Superposition theorem proving for commutative rings
In: Automated Deduction - A Basis for Applications. Volume III. Applications, 31-55 | Part of a Book | |
| 1 |
| |
| | 2007 | [Podelski, Andreas]
Wagner, Silke | | A Sound and Complete Proof Rule for Region Stability of Hybrid Systems
In: Hybrid systems: computation and control : 10th International Conference, HSCC 2007, 750-753 | Poster | |
| 1 |
| |
| | 1997 | [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 | Proceedings Article | |
| 2 |
| |
| | 2006 | [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, ??-?? | Proceedings Article | |
| | 2005 | [Yuan, Cong]
[Billington, Jonathan]
Freiheit, Jörn | | An 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 | Proceedings Article | |
| 1 |
| Bittanti, Sergio (ed.) |
| |
| | 2004 | Ratschan, Stefan
Vehi, Josep | | Robust 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 | Proceedings Article | |
| 3 |
| Biundo, Susanne (ed.) |
| |
| | 2005 | 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 | Proceedings Article | |
| | 2004 | [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 | Proceedings Article | |
| | 2004 | 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 | Proceedings Article | |
| 1 |
| Bjorner, Dines (ed.) |
| |
| | 2001 | 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 | Proceedings Article | |
| 6 |
| Blackburn, Patrick |
| |
| | 2001 | de Nivelle, Hans
[Blackburn, Patrick]
[Bos, Johan]
[Kohlhase, Michael] | | Inference and Computational Semantics
In: Studies in Linguistics and Philosophy, Computing Meaning [77], 11-28 | Journal Article | |
| | 1999 | [Blackburn, Patrick]
Tzakova, Miroslava | | Hybrid Languages and Temporal Logic
In: Logic Journal of the IGPL [7], 27-54 | Journal Article | |
| | 1998 | [Blackburn, Patrick]
Tzakova, Miroslava | | A Hybrid Concept Language
In: Proceedings of the 5th International Symposium on Artificial Intelligence and Mathematics, ? | Proceedings Article | |
| | 1998 | [Blackburn, Patrick]
Tzakova, Miroslava | | Hybrid Completeness
In: Logic Journal of the IGPL [6], 625-650 | Journal Article | |
| | 1998 | [Blackburn, Patrick]
Tzakova, Miroslava | | Hybrid Languages and Temporal Logic (Full Version) | Report | |
| | 1998 | [Blackburn, Patrick]
Tzakova, Miroslava | | Hybridizing Concept Languages
In: Annals of Mathematics and Artificial Intelligence [24], 23-49 | Journal Article | |
| 1 |
| |
| | 2003 | 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 | Proceedings Article | |
| 2 |
| |
| | 2005 | Blanchet, Bruno
Podelski, Andreas | | Verification of Cryptographic Protocols: Tagging Enforces Termination
In: Theoretical Computer Science [333], 67-90 | Journal Article | |
| | 2003 | 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 | Proceedings Article | |
| 1 |
| Bläsius, K. H. (ed.) |
| |
| | 1992 | Nonnengart, Andreas
Ohlbach, Hans Jürgen | | Modal- und Temporallogik
In: Deduktionssysteme - Automatisierung des logischen Denkens, 239-284 | Part of a Book | |
| 1 |
| Bläsius, K.H. (ed.) |
| |
| | 1992 | [Eisinger, Norbert]
Nonnengart, Andreas
[Präcklein, Axel] | | Termersetzungssysteme
In: Deduktionssysteme -- Automatisierung des logischen Denkens, 126-149 | Part of a Book | |
| 1 |
| Bla, Blubber (ed.) |
| |
| | 2009 | Meter, Peter | | Just a test entry
In: Booktitle, 1001-1010 | Proceedings Article | |
| 1 |
| Blubber, Bla (ed.) |
| |
| | 2009 | Meter, Peter | | Just a test entry
In: Booktitle, 1001-1010 | Proceedings Article | |
| 37 |
| Bockmayr, Alexander |
| |
| | 2001 | [Bockmayr, Alexander]
Eisenbrand, Friedrich | | Cutting planes and the elementary closure in fixed dimension
In: Mathematics of Operations Research [26], 304-312 | Journal Article | |
| | 2001 | Bockmayr, Alexander
[Weispfenning, V.] | | Solving numerical constraints
In: Handbook of Automated Reasoning, 751-842 | Part of a Book | |
| | 2000 | 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 | Proceedings Article | |
| | 1999 | 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 | Journal Article | |
| | 1998 | 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 | Journal Article | |
| | 1998 | [Werner, Andreas]
Bockmayr, Alexander
[Krischer, Stefan] | | How to realize LSE narrowing
In: New Generation Computing [16], 397-434 | Journal Article | |
| | 1998 | Bockmayr, Alexander
Dimopoulos, Yannis | | Mixed Integer Programming Models for Planning Problems
In: Proceedings of the Workshop on Constraint Problem Reformulation (CP-98), 1-6 | Proceedings Article | |
| | 1998 | [Barth, Peter]
Bockmayr, Alexander | | Modelling Discrete Optimisation Problems in Constraint Logic Programming
In: Annals of Operations Research [81], 467-496 | Journal Article | |
| | 1997 | Barth, Peter
Bockmayr, Alexander | | PLAM: ProLog and Algebraic Modelling
In: Proceedings of the 5th International Conference on the Practical Application of Prolog, 73-82 | Proceedings Article | |
| | 1996 | Bockmayr, Alexander | | Constraints in functional logic programming (Abstract)
In: Integration of functional and logic languages, 4 | Proceedings Article | |
| | 1996 | Bockmayr, Alexander | | Gleichheit und Constraints in der Logikprogrammierung
Universität des Saarlandes | Thesis - Habilitation thesis | |
| | 1996 | Bockmayr, Alexander
Barth, Peter
Kasper, Thomas | | Methods and Tools for Pseudo-Boolean Problems
In: 2. Workshop Boolesche Probleme, 105-109 | Proceedings Article | |
| | 1996 | 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 | Proceedings Article | |
| | 1996 | Bockmayr, Alexander
Kasper, Thomas | | Pseudo-Boolean and Finite Domain Constraint Programming: A Case Study
In: Deklarative Constraint Programmierung, 29-41 | Proceedings Article | |
| | 1995 | 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 | Proceedings Article | |
| | 1995 | Bockmayr, Alexander
[Werner, Andreas] | | LSE narrowing for decreasing conditional term rewrite systems
In: Conditional Term Rewriting Systems CTRS'94, 51-70 | Proceedings Article | |
| | 1995 | Bockmayr, Alexander
[Krischer, Stefan]
[Werner, Andreas] | | Narrowing strategies for arbitrary canonical systems
In: Fundamenta Informaticae [24], 125-155 | Journal Article | |
| | 1995 | Barth, Peter
Bockmayr, Alexander | | Pseudo-Boolean Constraint Logic Programming
In: Computational Logic. The Newsletter of the European Network in Computational Logic [2], 52-53 | Journal Article | |
| | 1995 | Bockmayr, Alexander | | Solving pseudo-Boolean constraints
In: Constraint Programming: Basics and Trends, 22-38 | Proceedings Article | |
| | 1994 | Bockmayr, Alexander | | Cutting planes in constraint logic programming (Abstract)
In: Proceedings of the 3rd International Symposium Artificial Intelligence and Mathematics, | Proceedings Article | |
| | 1994 | Barth, Peter
Bockmayr, Alexander | | Global Consistency in CLP($\cal PB$)
In: Proceedings of the 10th Workshop Logic Programming WLP'94, 4 | Proceedings Article | |
| | 1994 | [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 | Proceedings Article | |
| | 1994 | Bockmayr, Alexander | | Using Strong Cutting Planes in Constraint Logic Programming (Extended Abstract)
In: Operations Research '93, 18th Symposium on Operations Research, 47-49 | Proceedings Article | |
| | 1993 | Bockmayr, Alexander | | 0-1 Constraints and 0-1 Optimization
In: 3rd Workshop on Constraint Logic Programming (WCLP '93), ? | Proceedings Article | |
| | 1993 | Werner, Andreas
Bockmayr, Alexander
Krischer, Stefan | | A Concept for the Implementation of LSE Narrowing
In: 9.~Workshop Logische Programmierung, ? | Proceedings Article | |
| | 1993 | Bockmayr, Alexander | | Conditional Narrowing Modulo a Set of Equations
In: Applicable Algebra in Engineering, Communication and Computing [4], 147-168 | Journal Article | |
| | 1993 | Bockmayr, Alexander | | Embedding OR Techniques in Constraint Logic Programming
In: Operations Research '92. 17th Symposium on Operations Research, 252-254 | Proceedings Article | |
| | 1993 | Werner, Andreas
Bockmayr, Alexander
Krischer, Stefan | | How to Realize LSE Narrowing | Report | |
| | 1993 | Werner, Andreas
Bockmayr, Alexander
Krischer, Stefan | | How to Realize LSE Narrowing
In: Proceedings of the 2nd International Workshop on Functional/Logic Programming, ?-? | Proceedings Article | |
| | 1993 | 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 | Proceedings Article | |
| | 1993 | Bockmayr, Alexander | | Logic Programming with Pseudo-Boolean Constraints
In: Constraint Logic Programming---Selected Research, 327-350 | Proceedings Article | |
| | 1993 | Barth, Peter
Bockmayr, Alexander | | Solving 0-1 Problems in CLP($\cal PB$)
In: Proceedings 9th Conference on Artificial Intelligence for Applications (CAIA), 263-269 | Proceedings Article | |
| | 1992 | Bockmayr, Alexander | | A Theoretical Basis for Constraint Logic and Functional Programming
In: Proc.~1st African Conference on Research in Computer Science, 793-804 | Proceedings Article | |
| | 1992 | Bockmayr, Alexander | | Algebraic and Logical Aspects of Unification
In: Proc.~1st Workshop on Word Equations and Related Topics, 171-180 | Proceedings Article | |
| | 1992 | Bockmayr, Alexander | | Model-Theoretic Aspects of Unification
In: Proceedings of the 1st Workshop on Word Equations and Related Topics, 181-196 | Proceedings Article | |
| | 1991 | 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 | Proceedings Article | |
| | 1991 | 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 | Journal Article | |
| 1 |
| Boley, H. (ed.) |
| |
| | 1991 | Hanus, Michael | | Efficient Implementation of Narrowing and Rewriting
In: Proc. Intern. Workshop on Processing Declarative Knowledge, 344-365 | Proceedings Article | |
| 2 |
| Bonacina, Maria Paola (ed.) |
| |
| | 1997 | Waldmann, Uwe | | A Superposition Calculus for Divisible Torsion-Free Abelian Groups
In: Proceedings of the International Workshop on First-Order Theorem Proving (FTP-97), 130-134 | Proceedings Article | |
| | 1997 | Stuber, Jürgen | | Strong 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 | Proceedings Article | |
| 1 |
| |
| | 1991 | Socher-Ambrosius, Rolf | | Boolean Algebra Admits no Convergent Term Rewriting System
In: Proceedings of the 4th International Conference on Rewriting Techniques and Applications (RTA-91), 264-274 | Proceedings Article | |
| 1 |
| |
| | 1991 | 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 | Proceedings Article | |
| 2 |
| |
| | 2001 | Booth, Richard | | The lexicographic closure as a revision process
In: Journal of Applied Non-Classical Logics [11], 35-58 | Journal Article | |
| | 2000 | Booth, Richard | | The lexicographic closure as a revision process
In: Proceedings of the 8th International Workshop on Non-Monotonic Reasoning (NMR 2000), ? | Electronic Proceedings Article | |
| 1 |
| Borgida, A. (ed.) |
| |
| | 1995 | 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 | Proceedings Article | |
| 1 |
| Boros, Endre (ed.) |
| |
| | 1998 | [Blackburn, Patrick]
Tzakova, Miroslava | | A Hybrid Concept Language
In: Proceedings of the 5th International Symposium on Artificial Intelligence and Mathematics, ? | Proceedings Article | |
| 3 |
| Borrajo, Daniel (ed.) |
| |
| | 2006 | [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 | Proceedings Article | |
| | 2006 | 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 | Proceedings Article | |
| | 2006 | 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 | Proceedings Article | |
| 1 |
| Bosma, Wieb (ed.) |
| |
| | 2000 | 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 | Proceedings Article | |
| 1 |
| Bos, Johan |
| |
| | 2001 | de Nivelle, Hans
[Blackburn, Patrick]
[Bos, Johan]
[Kohlhase, Michael] | | Inference and Computational Semantics
In: Studies in Linguistics and Philosophy, Computing Meaning [77], 11-28 | Journal Article | |
| 1 |
| Böttner, Michael (ed.) |
| |
| | 2000 | Schmidt, Renate A. | | Relational Grammars for Knowledge Representation
In: Variable-Free Semantics, 162-180 | Part of a Book | |
| 1 |
| Boulmé, Sylvain |
| |
| | 2005 | Prevosto, Virgile
[Boulmé, Sylvain] | | Proof Contexts with Late Binding
In: Typed Lambda Calculi and Applications: 7th International Conference, TLCA 2005, 325-339 | Proceedings Article | |
| 1 |
| Bozkurt, Ahmet |
| |
| | 1995 | Bozkurt, Ahmet | | Strategien für Resolutionsbeweiser in Logik höherer Stufe
Universität des Saarlandes | Thesis - Masters thesis | |
| 2 |
| Bozzano, Marco |
| |
| | 1999 | [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 | Part of a Book | |
| | 1999 | [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 | Proceedings Article | |
| 1 |
| |
| | 2002 | de Nivelle, Hans | | Extraction 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 | Proceedings Article | |
| 2 |
| |
| | 2005 | 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 | Proceedings Article | |
| | 2004 | [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 | Proceedings Article | |
| 1 |
| Brafman, Ronen I. |
| |
| | 2006 | Hoffmann, Jörg
[Brafman, Ronen I.] | | Conformant planning via heuristic forward search: A new approach
In: Artificial Intelligence [170], 507-541 | Journal Article | |
| 5 |
| Brahm, Uwe |
| |
| | 2013 | Brahm, Uwe | | Möglichkeiten des Groupware-Einsatzes im Umfeld des Wissenschaftlerarbeitsplatzes am Beispiel des Max-Planck-Instituts für Informatik
Universität des Saarlandes | Thesis - Masters thesis | |
| | 2006 | Brahm, Uwe | | Eine integrierte Publikationsverwaltung am Beispiel des Max-Planck-Instituts für Informatik | Miscellaneous | |
| | 2002 | Weidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor | | SPASS Version 2.0
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 275-279 | Proceedings Article | |
| | 1999 | 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 | Proceedings Article | |
| | 1990 | Brahm, Uwe
[Pitz, Werner] | | Parkwächter
In: c't Magazin für computer technik [-], 252-253 | Journal Article | |
| 1 |
| Brauer, Wilfried (ed.) |
| |
| | 1995 | Weydert, Emil | | Default 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 | Proceedings Article | |
| 3 |
| Brewka, Gerd (ed.) |
| |
| | 1999 | Weydert, Emil | | JZBR - 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 | Proceedings Article | |
| | 1997 | | | Proceedings of the 3rd Dutch/German Workshop on Nonmonotonic Reasoning Techniques and their Applications (DGNMR-97) | Proceedings | |
| | 1997 | Weydert, Emil | | Qualitative Entropy Maximization - A preliminary report
In: Proceedings of the 3rd Dutch/German Workshop on Nonmonotonic Reasoning Techniques and their Applications (DGNMR-97), 63-72 | Proceedings Article | |
| 3 |
| Brewka, Gerhard (ed.) |
| |
| | 2001 | Weydert, Emil | | Rankings 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 | Proceedings Article | |
| | 1997 | 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 | Proceedings Article | |
| | 1997 | 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 | Proceedings Article | |
| 2 |
| Brim, Lubos (ed.) |
| |
| | 2002 | 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 | Proceedings Article | |
| | 1998 | Vorobyov, Sergei | | $\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 | Proceedings Article | |
| 1 |
| |
| | 2000 | Brinker, Christof | | Geometrisches Schließen mit SPASS
Universität des Saarlandes | Thesis - Masters thesis | |
| 4 |
| |
| | 1994 | [Brink, Chris]
[Britz, Katarina]
Schmidt, Renate A. | | Peirce Algebras
In: Formal Aspects of Computing [6], 339-358 | Journal Article | |
| | 1994 | [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 | Proceedings Article | |
| | 1994 | [Brink, Chris]
Gabbay, Dov M.
Ohlbach, Hans Jürgen | | Towards Automating Duality
In: Journal of Computers and Mathematics with Applications [29], 73-90 | Journal Article | |
| | 1991 | [Brink, Chris]
[Rewitzky, I. M.]
Schmidt, Renate A. | | Autodescriptivity: Beware!
In: The Computer Journal [34], 380-381 | Journal Article | |
| 1 |
| Brink, C. (ed.) |
| |
| | 1994 | 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 | Proceedings Article | |
| 2 |
| Britz, Katarina |
| |
| | 1994 | [Brink, Chris]
[Britz, Katarina]
Schmidt, Renate A. | | Peirce Algebras
In: Formal Aspects of Computing [6], 339-358 | Journal Article | |
| | 1994 | [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 | Proceedings Article | |
| 1 |
| |
| | 1994 | Weidenbach, Christoph | | First-Order Tableaux with Sorts
In: TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 247-261 | Proceedings Article | |
| 1 |
| |
| | 1992 | 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 | Proceedings Article | |
| 1 |
| |
| | 1991 | 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 | Journal Article | |
| 1 |
| |
| | 2001 | 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 | Proceedings Article | |
| 2 |
| Bruynooghe, Maurice (ed.) |
| |
| | 1993 | 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 | Proceedings Article | |
| | 1992 | Hanus, Michael | | Improving Control of Logic Programs by Using Functional Logic Languages
In: Proceedings 4th International Symposium on Programming Language Implementation and Logic Programming, 1-23 | Proceedings Article | |
| 1 |
| Brzoska, C. |
| |
| | 1991 | 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 | Journal Article | |
| 1 |
| Buchanan, George (ed.) |
| |
| | 2005 | Freiheit, Jörn
[Münch, Susanne]
[Schöttle, Hendrik]
[Sijanski, Grozdana]
[Zangl, Fabrice] | | Enhanced 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 | Proceedings Article | |
| 1 |
| Buchheit, Martin (ed.) |
| |
| | 1994 | Hustadt, Ullrich | | Do 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 | Proceedings Article | |
| 1 |
| Buchmann, Johannes |
| |
| | 1999 | [Buchmann, Johannes]
Eisenbrand, Friedrich | | On Factor Refinement in Number Fields
In: Mathematics of Computation [68], 345-350 | Journal Article | |
| 1 |
| Buchmann, J. (ed.) |
| |
| | 1992 | 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 | Part of a Book | |
| 1 |
| Bugliesi, Michele |
| |
| | 2000 | [Bugliesi, Michele]
Delzanno, Giorgio
[Liquori, Luigi]
[Martelli, Maurizio] | | Object Calculi in Linear Logic
In: Journal of Logic and Computation [10], 75-104 | Journal Article | |
| 11 |
| Bundy, Alan |
| |
| | 1999 | Madden, Peter
[Bundy, Alan]
[Smaill, Alan] | | Recursive Program Optimization Through Inductive Synthesis Proof Transformation
In: Journal of Automated Reasoning [22], 65-115 | Journal Article | |
| | 1996 | [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 | Proceedings Article | |
| | 1996 | [Kraan, Ina]
Basin, David A.
[Bundy, Alan] | | Middle-Out Reasoning for Synthesis and Induction
In: Automated mathematical induction, 113-145 | Part of a Book | |
| | 1996 | [Kraan, Ina]
Basin, David A.
[Bundy, Alan] | | Middle-out reasoning for synthesis and induction
In: Journal of Automated Reasoning [16], 113-145 | Journal Article | |
| | 1995 | Bundy, Alan
[Lombart, V.] | | Relational Rippling: a General Approach
In: Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence (IJCAI-95), 175-181 | Proceedings Article | |
| | 1994 | [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 | Proceedings Article | |
| | 1993 | 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 | Proceedings Article | |
| | 1993 | 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, | Proceedings Article | |
| | 1993 | 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 | Proceedings Article | |
| | 1993 | 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 | Proceedings Article | |
| | 1992 | 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 | Proceedings Article | |
| 7 |
| Bundy, Alan (ed.) |
| |
| | 1995 | Graf, Peter | | Substitution Tree Indexing
In: Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95), 117-131 | Proceedings Article | |
| | 1994 | Socher-Ambrosius, Rolf | | A Refined Version of General E-Unification
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 665-677 | Proceedings Article | |
| | 1994 | Graf, Peter | | Extended Path-Indexing
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 514-528 | Proceedings Article | |
| | 1994 | Bachmair, Leo
Ganzinger, Harald | | Ordered Chaining for Total Orderings
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 435-450 | Proceedings Article | |
| | 1994 | [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 | Proceedings Article | |
| | 1994 | Basin, David A.
[Walsh, Toby] | | Termination Orderings for Rippling
In: Proceedings of the 12th International Conference On Automated Deduction (CADE-12), 466-483 | Proceedings Article | |
| | 1994 | Plaisted, David A. | | The Search Efficiency of Theorem Proving Strategies
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 57-71 | Proceedings Article | |
| 1 |
| Burchardt, Aljoscha |
| |
| | 2004 | Baumgartner, Peter
[Burchardt, Aljoscha] | | Logic Programming Infrastructure for Inferences on FrameNet
In: Logics in artificial intelligence : 9th European Conference, JELIA 2004, 591-603 | Proceedings Article | |
| 3 |
| Bürckert, Hans-Jürgen (ed.) |
| |
| | 1993 | Hustadt, Ullrich | | Automated Support for the Development of Non-classical Logics
In: Workshop: Modellierung epistemischer Propositionen, KI '93, | Proceedings Article | |
| | 1992 | Nonnengart, Andreas
Ohlbach, Hans Jürgen | | Modal- und Temporallogik
In: Deduktionssysteme - Automatisierung des logischen Denkens, 239-284 | Part of a Book | |
| | 1992 | [Eisinger, Norbert]
Nonnengart, Andreas
[Präcklein, Axel] | | Termersetzungssysteme
In: Deduktionssysteme -- Automatisierung des logischen Denkens, 126-149 | Part of a Book | |
| 1 |
| Burkard, Rainer E. (ed.) |
| |
| | 1999 | 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 | Proceedings Article | |
| 1 |
| Buttazzo, Giorgio C. (ed.) |
| |
| | 2007 | [Podelski, Andreas]
Wagner, Silke | | A Sound and Complete Proof Rule for Region Stability of Hybrid Systems
In: Hybrid systems: computation and control : 10th International Conference, HSCC 2007, 750-753 | Poster | |
| 1 |
| Cachro, Jacek (ed.) |
| |
| | 1999 | Sofronie-Stokkermans, Viorica | | Resolution-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 | Proceedings Article | |
| 2 |
| Calmet, Jacques (ed.) |
| |
| | 2006 | 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 | Proceedings Article | |
| | 1995 | 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 | Proceedings Article | |
| 1 |
| |
| | 2003 | Kazakov, Yevgeny
de Nivelle, Hans | | Subsumption 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 | Proceedings Article | |
| 1 |
| |
| | 1996 | [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 | Proceedings Article | |
| 1 |
| |
| | 1995 | 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 | Proceedings Article | |
| 1 |
| |
| | 1996 | [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 | Proceedings Article | |
| 1 |
| |
| | 1996 | Graf, Peter | | Term Indexing | Book | |
| 2 |
| Carlucci-Aiello, Luigia (ed.) |
| |
| | 1996 | 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 | Proceedings Article | |
| | 1996 | Jaeger, Manfred | | Representation Independence of Nonmonotonic Inference Relations
In: Principles of Knowledge Representation and Reasoning, Proceedings of the 5th International Conference (KR-96), 461-472 | Proceedings Article | |
| 1 |
| Cassandras, Christos (ed.) |
| |
| | 2006 | Ratschan, Stefan
[Smaus, Jan-Georg] | | Verification-Integrated Falsification of Non-Deterministic Hybrid Systems
In: 2nd IFAC Conference on Analysis and Design of Hybrid Systems, ? | Proceedings Article | |
| 2 |
| Cavalcanti, Ana (ed.) |
| |
| | 2006 | [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 | Proceedings Article | |
| | 2006 | 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 | Proceedings Article | |
| 1 |
| |
| | 1999 | van der Torre, Leendert W. N.
[Tan, Yao-Hua] | | Contextual Deontic Logic: violation contexts and factual defeasibility
In: Formal Aspects in Context, 173-192 | Part of a Book | |
| 1 |
| |
| | 2005 | Freiheit, Jörn
[Münch, Susanne]
[Schöttle, Hendrik]
[Sijanski, Grozdana]
[Zangl, Fabrice] | | Enhanced 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 | Proceedings Article | |
| 2 |
| |
| | 2006 | [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 | Proceedings Article | |
| | 2006 | 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 | Proceedings Article | |
| 2 |
| Chadha, Ritu |
| |
| | 1994 | [Chadha, Ritu]
Plaisted, David A. | | Correctness of unification without occur check in Prolog
In: Journal of Logic Programming [18], 99-122 | Journal Article | |
| | 1993 | Chadha, Ritu
Plaisted, David A. | | On the mechanical derivation of loop invariants
In: Journal of Symbolic Computation [15], 705-744 | Journal Article | |
| 23 |
| |
| | 2005 | [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 | Proceedings Article | |
| | 2003 | Charatonik, Witold
[Dal Zilio, Silvano]
[Gordon, Andrew Donald]
[Mukhopadhyay, Supratik]
[Talbot, Jean-Marc] | | Model checking mobile ambients
In: Theoretical Computer Science [308], 277-331 | Journal Article | |
| | 2002 | Charatonik, Witold
[Talbot, Jean-Marc] | | Atomic Set Constraints with Projection
In: Rewriting Techniques and Applications. 13th International Conference, RTA 2002, 311-325 | Proceedings Article | |
| | 2002 | 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 | Proceedings Article | |
| | 2002 | 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 | Proceedings Article | |
| | 2002 | Charatonik, Witold | | Direktionale Typen in der Logischen Programmierung
Universität des Saarlandes | Thesis - Habilitation thesis | |
| | 2002 | 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 | Proceedings Article | |
| | 2002 | 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 | Proceedings Article | |
| | 2002 | Charatonik, Witold
Podelski, Andreas | | Set Constraints with Intersection
In: Information and Computation [179], 213-229 | Journal Article | |
| | 2001 | Charatonik, Witold
[Dal Zilio, Silvano]
[Gordon, Andrew Donald]
Mukhopadhyay, Supratik
[Talbot, Jean-Marc] | | The Complexity of Model Checking Mobile Ambients | Report | |
| | 2001 | 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 | Proceedings Article | |
| | 2001 | 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 | Proceedings Article | |
| | 2000 | Charatonik, Witold | | Directional Type Checking for Logic Programs: Beyond Discriminative Types
In: Proceedings of the 8th European Symposium on Programming (ESOP-00), 72-87 | Proceedings Article | |
| | 2000 | 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 | Proceedings Article | |
| | 1999 | 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 | Proceedings Article | |
| | 1998 | Charatonik, Witold | | An Undecidable Fragment of the Theory of Set Constraints
In: Information Processing Letters [68], 147-151 | Journal Article | |
| | 1998 | Charatonik, Witold
Podelski, Andreas | | Co-definite Set Constraints
In: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), 211-225 | Proceedings Article | |
| | 1998 | Charatonik, Witold
Podelski, Andreas | | Directional Type Inference for Logic Programs
In: Proceedings of the 5th International Symposium in Static Analysis (SAS-98), 278-294 | Proceedings Article | |
| | 1998 | 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 | Proceedings Article | |
| | 1998 | Charatonik, Witold | | Set Constraints in Some Equational Theories
In: Information and Computation [142], 40-75 | Journal Article | |
| | 1998 | 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 | Proceedings Article | |
| | 1997 | 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 | Proceedings Article | |
| | 1996 | 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 | Proceedings Article | |
| 3 |
| |
| | 2002 | Maier, Patrick | | A Framework for Circular Assume-Guarantee Rules
In: Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, 55-58 | Proceedings Article | |
| | 2002 | Hillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor | | Is Logic Effective for Analyzing C Programs?
In: Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, 27-30 | Proceedings Article | |
| | 2002 | Kazakov, Yevgeny | | Recursive resolution for modal logic
In: Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, 11-15 | Proceedings Article | |
| 1 |
| |
| | 1996 | Chaudhuri, Shiva
Dimopoulos, Yannis
Zaroliagis, Christos | | On the Parallel Complexity of Acyclic Logic Programs
In: Parallel Processing Letters [6], 223-230 | Journal Article | |
| 1 |
| |
| | 1993 | 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 | Proceedings Article | |
| 1 |
| |
| | 1997 | Christen, Michael | | A Calculus of Simplification for Superposition
Universität des Saarlandes | Thesis - Masters thesis | |
| 1 |
| |
| | 1994 | [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 | Proceedings Article | |
| 1 |
| Cialdea Mayer, Marta (ed.) |
| |
| | 2003 | [Letz, Reinhold]
Stenz, Gernot | | Universal variables in disconnection tableaux
In: Automated reasoning with analytical tableaux and related methods : International Conference, TABLEAUX 2003, 117-133 | Proceedings Article | |
| 1 |
| |
| | 1999 | Sofronie-Stokkermans, Viorica
[Stokkermans, Karel] | | Modeling Interaction by Sheaves and Geometric Logic
In: Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99), 512-523 | Proceedings Article | |
| 2 |
| |
| | 1993 | Fehrer, Detlef | | A Unifying Framework for Reason Maintenance
In: Symbolic and Quantitative Approaches to Reasoning and Uncertainty: Proceedings European Conference ECSQARU '93, 113-120 | Proceedings Article | |
| | 1993 | Weydert, Emil | | Plausible Inference for Default Conditionals
In: Symbolic and Quantitative Approaches to Reasoning and Uncertainty: Proceedings of the European Conference ECSQARU '93, 356-363 | Proceedings Article | |
| 3 |
| Claus, Volker (ed.) |
| |
| | 1996 | | | Evolutionary Algorithms and their Application | Report | |
| | 1996 | Hopf, Jörn | | Optimizing Photo Mask Layout for Grey-tone Lithography | Report | |
| | 1996 | Hopf, Jörn | | Optimizing Photo Mask Layout for Grey-tone Lithography | Report | |
| 1 |
| Cleaveland, Rance (ed.) |
| |
| | 1999 | 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 | Proceedings Article | |
| 1 |
| Clement, T. (ed.) |
| |
| | 1993 | 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 | Proceedings Article | |
| 1 |
| Codognet, P. (ed.) |
| |
| | 1993 | Hustadt, Ullrich | | Abductive Disjunctive Logic Programming
In: ICLP '93 Postconference Workshop on Abductive Reasoning, ? | Proceedings Article | |
| 2 |
| Cohn, Anthony G. (ed.) |
| |
| | 1998 | Jaeger, Manfred | | Reasoning 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 | Proceedings Article | |
| | 1998 | Weydert, Emil | | System 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 | Proceedings Article | |
| 1 |
| |
| | 1994 | [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 | Proceedings Article | |
| 2 |
| |
| | 1999 | 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 | Proceedings Article | |
| | 1998 | Weidenbach, Christoph
Meyer, Christoph
Cohrs, Christian
Engel, Thorsten
Keen, Enno | | SPASS V0.77
In: Journal of Automated Reasoning [21], 113-113 | Journal Article | |
| 3 |
| Colmerauer, A. (ed.) |
| |
| | 1993 | Bockmayr, Alexander | | 0-1 Constraints and 0-1 Optimization
In: 3rd Workshop on Constraint Logic Programming (WCLP '93), ? | Proceedings Article | |
| | 1993 | Barth, Peter | | A Complete Symbolic 0-1 Constraint Solver
In: 3rd Workshop on Constraint Logic Programming (WCLP '93), ? | Proceedings Article | |
| | 1993 | Bockmayr, Alexander | | Logic Programming with Pseudo-Boolean Constraints
In: Constraint Logic Programming---Selected Research, 327-350 | Proceedings Article | |
| 3 |
| Comon, Hubert (ed.) |
| |
| | 2001 | Ganzinger, Harald
[Nieuwenhuis, Robert] | | Constraints and Theorem Proving
In: Contraints in Computational Logics, International Summer School (CCL-99), 159-201 | Proceedings Article | |
| | 1997 | Struth, Georg | | On the Word Problem for Free Lattices
In: Proceedings of the 8th International Conference on Rewriting Techniques and Applications (RTA-97), 128-141 | Proceedings Article | |
| | 1997 | Vorobyov, Sergei | | The 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 | Proceedings Article | |
| 1 |
| Constable, Robert L. |
| |
| | 1993 | Basin, David A.
Constable, Robert L. | | Metalogical Frameworks
In: Logical Environments, 1-29 | Part of a Book | |
| 6 |
| Cook, Byron |
| |
| | 2007 | [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 | Proceedings Article | |
| | 2007 | [Cook, Byron]
[Podelski, Andreas]
Rybalchenko, Andrey | | Proving Thread Termination
In: PLDI'07 : Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 320-330 | Proceedings Article | |
| | 2006 | [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 | Proceedings Article | |
| | 2006 | Cook, Byron
Podelski, Andreas
Rybalchenko, Andrey | | Terminator: Beyond Safety
In: Computer aided verification : 18th International Conference, CAV 2006, 415-418 | Proceedings Article | |
| | 2005 | [Cook, Byron]
Podelski, Andreas
Rybalchenko, Andrey | | Abstraction-refinement for Termination
In: Static analysis : 12th International Symposium, SAS 2005, 87-101 | Proceedings Article | |
| | 2005 | Podelski, Andreas
Rybalchenko, Andrey
[Cook, Byron] | | Counterexample-Guided Abstraction Refinement for Termination | Unpublished/Draft | |
| 3 |
| |
| | 2007 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation
In: 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007), ? | Proceedings Article | |
| | 2007 | [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 | Proceedings Article | |
| | 2006 | Jacobs, Swen
Sofronie-Stokkermans, Viorica | | Applications of hierarchical reasoning in the verification of complex systems
In: PDPAR'06: Pragmatical Aspects of Decision Procedures in Automated Reasoning, 15-26 | Electronic Proceedings Article | |
| 1 |
| |
| | 1998 | Jaeger, Manfred | | Measure Selection: Notions of Rationality and Representation Independence
In: Proceedings of the 14th Conference on Uncertainty in Artificial Intelligence (UAI-98), 274-281 | Proceedings Article | |
| 1 |
| |
| | 2006 | Prevosto, Virgile | | Certified mathematical hierarchies: the FoCal system.
In: Proceedings of the MAP (Mathematics, Algorithms, Proofs) Workshop, | Electronic Proceedings Article | |
| 1 |
| |
| | 1999 | 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 | Proceedings Article | |
| 2 |
| |
| | 2003 | Podelski, Andreas | | Software Model Checking with Abstraction Refinement
In: Verification, model checking, and abstract interpretation : 4th International Conference, VMCAI 2003, 1-13 | Proceedings Article | |
| | 2002 | 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 | Proceedings Article | |
| 1 |
| Cortier, V. |
| |
| | 1999 | 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 | Proceedings Article | |
| 2 |
| Cunningham, Jim (ed.) |
| |
| | 2000 | Weydert, Emil | | Rankings in flux
In: Proceedings of the 3rd International Conference on Formal and Applied Practical Reasoning (FAPR-00), 37-48 | Proceedings Article | |
| | 1994 | Fehrer, Detlef | | A Unifying Logical Framework for Reason Maintenance (Deliverable DI.1.2-3P)
In: Medlar II Report PPR2, 47-55 | Proceedings Article | |
| 1 |
| |
| | 1991 | Cunningham, J.
Gabbay, Dov M.
Ohlbach, Hans Jürgen | | Towards the MEDLAR Framework
In: ESPRIT '91 Conference Proceedings, 822-841 | Proceedings Article | |
| 1 |
| |
| | 2005 | [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 | Proceedings Article | |
| 1 |
| D'Agostino, Marcello (ed.) |
| |
| | 1994 | Weidenbach, Christoph | | First-Order Tableaux with Sorts
In: TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 247-261 | Proceedings Article | |
| 1 |
| |
| | 2000 | Mukhopadhyay, Supratik
Podelski, Andreas | | Model Checking for Timed Logic Processes
In: Proceedings of the 1st International Conference on Computational Logic, 598-612 | Proceedings Article | |
| 1 |
| |
| | 2003 | Hillenbrand, Thomas | | Citius 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 | Electronic Proceedings Article | |
| 3 |
| |
| | 2003 | Charatonik, Witold
[Dal Zilio, Silvano]
[Gordon, Andrew Donald]
[Mukhopadhyay, Supratik]
[Talbot, Jean-Marc] | | Model checking mobile ambients
In: Theoretical Computer Science [308], 277-331 | Journal Article | |
| | 2001 | Charatonik, Witold
[Dal Zilio, Silvano]
[Gordon, Andrew Donald]
Mukhopadhyay, Supratik
[Talbot, Jean-Marc] | | The Complexity of Model Checking Mobile Ambients | Report | |
| | 2001 | 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 | Proceedings Article | |
| 2 |
| |
| | 2006 | [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 | Proceedings Article | |
| | 2005 | [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 | Proceedings Article | |
| 1 |
| Danvy, Olivier (ed.) |
| |
| | 2001 | Ganzinger, Harald | | Bottom-Up Deduction with Deletion and Priorities
In: Programs as Data Objects (PADO-01) : Second Symposium PADO 2001, 276-277 | Proceedings Article | |
| 1 |
| Dauchet, Max (ed.) |
| |
| | 1997 | [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 | Proceedings Article | |
| 1 |
| Daum, Matthias |
| |
| | 2005 | [Daum, Matthias]
Maus, Stefan
[Schirmer, Norbert]
Seghir, Mohammed Nassim | | Integration of a Software Model Checker into Isabelle
In: Logic for Programming, Artificial Intelligence, and Reasoning: 12th International Conference, LPAR 2005, 381-395 | Proceedings Article | |
| 1 |
| De Giacomo, Giuseppe (ed.) |
| |
| | 2003 | Kazakov, Yevgeny
de Nivelle, Hans | | Subsumption 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 | Proceedings Article | |
| 1 |
| de Leon, David (ed.) |
| |
| | 1999 | Weydert, Emil | | JZBR - Iterated Belief Change for Conditional Ranking Constraints
In: Spinning Ideas - Electronic Essays Dedicated to Peter Gaerdenfors on His Fiftieth Birthday, 1-11 | Part of a Book | |
| 1 |
| de Moor, Aldo (ed.) |
| |
| | 2005 | Freiheit, Jörn
[Münch, Susanne]
[Schöttle, Hendrik]
[Sijanski, Grozdana]
[Zangl, Fabrice] | | Enhanced 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 | Proceedings Article | |
| 26 |
| de Nivelle, Hans |
| |
| | 2006 | 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 | Electronic Proceedings Article | |
| | 2006 | de Nivelle, Hans
[Meng, Jia] | | Geo 2006j | Miscellaneous | |
| | 2006 | 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 | Proceedings Article | |
| | 2005 | 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 | Journal Article | |
| | 2005 | de Nivelle, Hans | | Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
In: Information and Computation [199], 24-54 | Journal Article | |
| | 2005 | 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 | Proceedings Article | |
| | 2004 | 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 | Proceedings Article | |
| | 2004 | de Nivelle, Hans
Kazakov, Yevgeny | | Resolution Decision Procedures for the Guarded Fragment with
Transitive Guards | Report | |
| | 2003 | 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 | Proceedings Article | |
| | 2003 | de Nivelle, Hans
[Demri, Stéphane] | | Deciding regular grammar logics with converse through first-order logic | Report | |
| | 2003 | de Nivelle, Hans
[de Rijke, Maarten] | | Deciding the Guarded Fragments by Resolution
In: Journal of Symbolic Computation [35], 21-58 | Journal Article | |
| | 2003 | de Nivelle, Hans | | Implementing the clausal normal form transformation with proof generation
In: Fourth Workshop on the Implementation of Logics, 69-83 | Proceedings Article | |
| | 2003 | Kazakov, Yevgeny
de Nivelle, Hans | | Subsumption 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 | Proceedings Article | |
| | 2003 | de Nivelle, Hans | | Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 365-379 | Proceedings Article | |
| | 2002 | [Bezem, Marc]
[Hendriks, Dimitri]
de Nivelle, Hans | | Automated Proof Construction in Type Theory using Resolution
In: Journal of Automated Reasoning [29], 253-275 | Journal Article | |
| | 2002 | de Nivelle, Hans | | Extraction 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 | Proceedings Article | |
| | 2001 | 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 | Proceedings Article | |
| | 2001 | de Nivelle, Hans
[Blackburn, Patrick]
[Bos, Johan]
[Kohlhase, Michael] | | Inference and Computational Semantics
In: Studies in Linguistics and Philosophy, Computing Meaning [77], 11-28 | Journal Article | |
| | 2001 | [Areces, Carlos]
[de Rijke, Maarten]
de Nivelle, Hans | | Resolution in modal, description and hybrid logic
In: Journal of Logic and Computation [11], 717-736 | Journal Article | |
| | 2001 | de Nivelle, Hans | | Splitting through New Proposition Symbols
In: Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001), 172-185 | Proceedings Article | |
| | 2000 | de Nivelle, Hans | | An Overview of Resolution Decision Procedures
In: Formalizing the Dynamics of Information, 115-130 | Proceedings Article | |
| | 2000 | 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 | Proceedings Article | |
| | 2000 | de Nivelle, Hans | | Deciding the E-plus class by an a posteriori, liftable order
In: Annals of Pure and Applied Logic [88], 219-232 | Journal Article | |
| | 2000 | de Nivelle, Hans
Hustadt, Ullrich
[Schmidt, Renate A.] | | Resolution-Based Methods for Modal Logics
In: Logic Journal of the IGPL [8], 265-292 | Journal Article | |
| | 1999 | Ganzinger, Harald
de Nivelle, Hans | | A 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 | Proceedings Article | |
| | 1999 | 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 | Proceedings Article | |
| 5 |
| |
| | 2006 | 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 | Electronic Proceedings Article | |
| | 2006 | | | IJCAR'06 Workshop : Disproving'06: Non-Theorems, Non-Validity, Non-Provability | Electronic Proceedings | |
| | 2006 | Hillenbrand, Thomas
Topic, Dalibor
Weidenbach, Christoph | | Sudokus as Logical Puzzles
In: Proceedings of the Third Workshop on Disproving, 2-12 | Electronic Proceedings Article | |
| | 2001 | | | Proceedings of the 2nd International Workshop on the Implementation of Logics | Proceedings | |
| | 2001 | Hillenbrand, Thomas
[Löchner, Bernd] | | The Next WALDMEISTER Loop (Extended Abstract)
In: Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001, 13-21 | Proceedings Article | |
| 1 |
| |
| | 2002 | [de Raedt, Luc]
Jaeger, Manfred
[Lee, Sau Dan]
[Mannila, Heikki] | | A Theory of Inductive Query Answering
In: Proceedings of the 2002 IEEE International Conference on Data Mining (ICDM'02), 123-130 | Proceedings Article | |
| 3 |
| |
| | 2003 | de Nivelle, Hans
[de Rijke, Maarten] | | Deciding the Guarded Fragments by Resolution
In: Journal of Symbolic Computation [35], 21-58 | Journal Article | |
| | 2001 | [Areces, Carlos]
[de Rijke, Maarten]
de Nivelle, Hans | | Resolution in modal, description and hybrid logic
In: Journal of Logic and Computation [11], 717-736 | Journal Article | |
| | 1999 | 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 | Proceedings Article | |
| 1 |
| |
| | 2001 | Ganzinger, Harald
Hustadt, Ullrich
Meyer, Christoph
Schmidt, Renate A. | | A Resolution-Based Decision Procedure for Extensions of K4
In: Advances in Modal Logic, Volume 2, 225-246 | Part of a Book | |
| 1 |
| |
| | 1998 | Schmidt, Renate A. | | Resolution is a Decision Procedure for Many Propositional Modal Logics
In: Advances in Modal Logic, Volume 1, 189-208 | Part of a Book | |
| 2 |
| |
| | 1998 | 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 | Proceedings Article | |
| | 1998 | 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 | Proceedings Article | |
| 2 |
| Degtyarev, Anatoli |
| |
| | 2000 | [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 | Journal Article | |
| | 1998 | [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 | Proceedings Article | |
| 1 |
| |
| | 2005 | [Delahaye, David]
[Jaume, Mathieu]
Prevosto, Virgile | | Coq, un outil pour l'enseignement
In: Technique et Science Informatiques [24], 1139-1160 | Journal Article | |
| 1 |
| |
| | 1998 | Weydert, Emil | | Minimal 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 | Proceedings Article | |
| 10 |
| |
| | 2001 | Delzanno, Giorgio
Podelski, Andreas | | Constraint-based Deductive Model Checking
In: International Journal on Software Tools for Technology Transfer (STTT) [3], 250-270 | Journal Article | |
| | 2001 | [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 | Proceedings Article | |
| | 2000 | [Bugliesi, Michele]
Delzanno, Giorgio
[Liquori, Luigi]
[Martelli, Maurizio] | | Object Calculi in Linear Logic
In: Journal of Logic and Computation [10], 75-104 | Journal Article | |
| | 2000 | 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 | Proceedings Article | |
| | 1999 | Delzanno, Giorgio
[Galmiche, Didier]
[Martelli, Maurizio] | | A specification logic for concurrent object-oriented programming
In: Mathematical Structures in Computer Science [9], 253-286 | Journal Article | |
| | 1999 | 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 | Proceedings Article | |
| | 1999 | [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 | Part of a Book | |
| | 1999 | 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 | Proceedings Article | |
| | 1999 | [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 | Proceedings Article | |
| | 1998 | Delzanno, Giorgio | | Specification of Term Rewriting in Linear Logic
In: Proceedings of Workshop on Proof-Search in Type-Theoretic Languages, ?? | Proceedings Article | |
| 3 |
| Demri, Stéphane |
| |
| | 2005 | 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 | Journal Article | |
| | 2003 | 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 | Proceedings Article | |
| | 2003 | de Nivelle, Hans
[Demri, Stéphane] | | Deciding regular grammar logics with converse through first-order logic | Report | |
| 1 |
| Dershowitz, Nachum (ed.) |
| |
| | 1995 | Bockmayr, Alexander
[Werner, Andreas] | | LSE narrowing for decreasing conditional term rewrite systems
In: Conditional Term Rewriting Systems CTRS'94, 51-70 | Proceedings Article | |
| 1 |
| Dershowitz, N. (ed.) |
| |
| | 1995 | Bachmair, Leo
Ganzinger, Harald | | Associative-Commutative Superposition
In: Proceedings of the 4th International Workshop on Conditional and Typed Rewrite Systems (CTRS-94), 1-14 | Proceedings Article | |
| 1 |
| Deussen, P. |
| |
| | 1991 | 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 | Journal Article | |
| 1 |
| Devienne, Philippe |
| |
| | 2000 | Talbot, Jean-Marc
[Devienne, Philippe]
[Tison, Sophie] | | Generalized Definite Set Constraints
In: Constraints [5], 161-202 | Journal Article | |
| 1 |
| Dierks, Henning |
| |
| | 2006 | [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 | Proceedings Article | |
| 1 |
| Dietz, Jan L.G. (ed.) |
| |
| | 2005 | Freiheit, Jörn
[Münch, Susanne]
[Schöttle, Hendrik]
[Sijanski, Grozdana]
[Zangl, Fabrice] | | Enhanced 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 | Proceedings Article | |
| 1 |
| Dillon, Tharam (ed.) |
| |
| | 2005 | Freiheit, Jörn
[Münch, Susanne]
[Schöttle, Hendrik]
[Sijanski, Grozdana]
[Zangl, Fabrice] | | Enhanced 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 | Proceedings Article | |
| 1 |
| Dimitrova, Rayna |
| |
| | 2006 | Dimitrova, Rayna | | Model Checking with Abstraction Refinement for Well-Structured Systems
Universität des Saarlandes | Thesis - Masters thesis | |
| 7 |
| Dimopoulos, Yannis |
| |
| | 1998 | Bockmayr, Alexander
Dimopoulos, Yannis | | Mixed Integer Programming Models for Planning Problems
In: Proceedings of the Workshop on Constraint Problem Reformulation (CP-98), 1-6 | Proceedings Article | |
| | 1996 | Dimopoulos, Yannis | | On Computing Logic Programs
In: Journal of Automated Reasoning [17], 259-289 | Journal Article | |
| | 1996 | Chaudhuri, Shiva
Dimopoulos, Yannis
Zaroliagis, Christos | | On the Parallel Complexity of Acyclic Logic Programs
In: Parallel Processing Letters [6], 223-230 | Journal Article | |
| | 1994 | Dimopoulos, Yannis
[Magirou, Vangelis] | | A Graph Theoretic Approach to Default Logic
In: Information and Computation [112], 239-256 | Journal Article | |
| | 1994 | Dimopoulos, Yannis | | Classical Methods in Nonmonotonic Reasoning
In: Proceedings of the 8th International Symposium on Methodologies for Intelligent Systems (ISMIS'94), 500-510 | Proceedings Article | |
| | 1994 | Dimopoulos, Yannis | | The Computational Value of Joint Consistency
In: Logics in Artificial Intelligence: Proceedings of the JELIA'94, 50-65 | Proceedings Article | |
| | 1993 | Dimopoulos, Yannis
Magirou, Vangelis
Papadimitriou, Christos | | On Kernels, Defaults and Even Graphs
In: Annals of Mathematics and Artificial Intelligence, | Journal Article | |
| 1 |
| Disch, Stefan |
| |
| | 2006 | [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 | Proceedings Article | |
| 2 |
| Dix, Jürgen (ed.) |
| |
| | 1998 | 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 | Proceedings Article | |
| | 1998 | 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 | Proceedings Article | |
| 1 |
| |
| | 2005 | Ratschan, Stefan | | Solving 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 | Proceedings Article | |
| 2 |
| |
| | 2006 | [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 | Proceedings Article | |
| | 2006 | 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 | Proceedings Article | |
| 2 |
| Doyle, Jon (ed.) |
| |
| | 1996 | 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 | Proceedings Article | |
| | 1996 | Jaeger, Manfred | | Representation Independence of Nonmonotonic Inference Relations
In: Principles of Knowledge Representation and Reasoning, Proceedings of the 5th International Conference (KR-96), 461-472 | Proceedings Article | |
| 1 |
| |
| | 1994 | Jaeger, Manfred | | Probabilistic Reasoning in Terminological Logics
In: Principles of Knowledge Representation an Reasoning: Proceedings of the 4th International Conference (KR94), 305-316 | Proceedings Article | |
| 1 |
| |
| | 2006 | [Dräge, Klaus]
[Finkbeiner, Bernd]
Podelski, Andreas | | Directed Model Checking with Distance-Preserving Abstractions
In: Model checking software : 13th International SPIN Workshop, 19-34 | Proceedings Article | |
| 2 |
| Dreschler-Fischer, Leonie (ed.) |
| |
| | 1995 | Barth, Peter
[Kleine Büning, Hans]
Weidenbach, Christoph | | Workshop CPL Computational Propositional Logic
In: KI-95 Activities: Workshops, Posters, Demos, 71-72 | Proceedings Article | |
| | 1994 | Madden, Peter | | Formal Methods for Automated Program Improvement
In: KI-94: Advances in Artificial Intelligence. Proceedings of the 18th German Annual Conference on Artificial Intelligence, 367-378 | Proceedings Article | |
| 1 |
| Dubois, Catherine |
| |
| | 2004 | [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 | Proceedings Article | |
| 1 |
| Dung, P. M. (ed.) |
| |
| | 1993 | Hustadt, Ullrich | | Abductive Disjunctive Logic Programming
In: ICLP '93 Postconference Workshop on Abductive Reasoning, ? | Proceedings Article | |
| 1 |
| Duval, Erik (ed.) |
| |
| | 2005 | Freiheit, Jörn
[Münch, Susanne]
[Schöttle, Hendrik]
[Sijanski, Grozdana]
[Zangl, Fabrice] | | Enhanced 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 | Proceedings Article | |
| 1 |
| Echahed, Rachid |
| |
| | 1994 | [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 | Proceedings Article | |
| 1 |
| Egly, Uwe (ed.) |
| |
| | 2002 | Sofronie-Stokkermans, Viorica | | On uniform word problems involving bridging operators on distributive lattices
In: Automated Reasoning with Analytic and Related Methods : International Conference, TABLEAUX 2002, 235-250 | Proceedings Article | |
| 11 |
| Eisenbrand, Friedrich |
| |
| | 2002 | 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 | Proceedings Article | |
| | 2001 | [Bockmayr, Alexander]
Eisenbrand, Friedrich | | Cutting planes and the elementary closure in fixed dimension
In: Mathematics of Operations Research [26], 304-312 | Journal Article | |
| | 2001 | 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 | Proceedings Article | |
| | 2001 | 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 | Proceedings Article | |
| | 2001 | Eisenbrand, Friedrich | | Short vectors of planar integral lattices via continued fractions
In: Information Processing Letters [79], 121-126 | Journal Article | |
| | 2000 | 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 | Proceedings Article | |
| | 2000 | Eisenbrand, Friedrich | | Gomory-Chvátal Cutting planes and the Elementary Closure of Polyhedra
Universität des Saarlandes | Thesis - PhD thesis | |
| | 1999 | 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 | Proceedings Article | |
| | 1999 | [Buchmann, Johannes]
Eisenbrand, Friedrich | | On Factor Refinement in Number Fields
In: Mathematics of Computation [68], 345-350 | Journal Article | |
| | 1999 | 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 | Journal Article | |
| | 1999 | Eisenbrand, Friedrich | | On the Membership Problem for the Elementary Closure of a Polyhedron
In: Combinatorica [19], 297-300 | Journal Article | |
| 3 |
| Eisinger, Norbert |
| |
| | 1993 | Eisinger, Norbert
Ohlbach, Hans Jürgen | | Deduction Systems Based on Resolution
In: Handbook of Logic in Artificial Intelligence and Logic Programming, 184-271 | Proceedings Article | |
| | 1992 | [Eisinger, Norbert]
Nonnengart, Andreas
[Präcklein, Axel] | | Termersetzungssysteme
In: Deduktionssysteme -- Automatisierung des logischen Denkens, 126-149 | Part of a Book | |
| | 1991 | Eisinger, Norbert
Ohlbach, Hans Jürgen
Präcklein, Axel | | Reduction Rules for Resolution Based Systems
In: Artificial Intelligence [50], 141-181 | Journal Article | |
| 1 |
| Eklund, Patrick (ed.) |
| |
| | 1998 | Sofronie-Stokkermans, Viorica | | Representation 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), ?-? | Proceedings Article | |
| 1 |
| Emerson, E. Allen (ed.) |
| |
| | 2006 | Wies, Thomas
[Kuncak, Viktor]
[Lam, Patrick]
Podelski, Andreas
[Rinard, Martin C.] | | Field Constraint Analysis
In: Verification, Model Checking, and Abstract Interpretation : 7th International Conference, VMCAI 2006, 157-173 | Proceedings Article | |
| 3 |
| Engel, Thorsten |
| |
| | 1999 | 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 | Proceedings Article | |
| | 1998 | Weidenbach, Christoph
Meyer, Christoph
Cohrs, Christian
Engel, Thorsten
Keen, Enno | | SPASS V0.77
In: Journal of Automated Reasoning [21], 113-113 | Journal Article | |
| | 1996 | Engel, Thorsten | | Quantifier Elimination in Second-Order Predicate Logic
Universität des Saarlandes | Thesis - Masters thesis | |
| 1 |
| Escalada-Imaz, Gonzalo (ed.) |
| |
| | 1998 | Sofronie-Stokkermans, Viorica | | Representation 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), ?-? | Proceedings Article | |
| 2 |
| Esparza, Javier |
| |
| | 2000 | [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 | Proceedings Article | |
| | 1999 | 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 | Proceedings Article | |
| 1 |
| |
| | 1994 | Bockmayr, Alexander | | Using Strong Cutting Planes in Constraint Logic Programming (Extended Abstract)
In: Operations Research '93, 18th Symposium on Operations Research, 47-49 | Proceedings Article | |
| 1 |
| |
| | 1994 | Weidenbach, Christoph | | First-Order Tableaux with Sorts
In: TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 247-261 | Proceedings Article | |
| 1 |
| |
| | 2006 | [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 | Proceedings Article | |
| 1 |
| |
| | 2000 | de Nivelle, Hans | | An Overview of Resolution Decision Procedures
In: Formalizing the Dynamics of Information, 115-130 | Proceedings Article | |
| 2 |
| Fariñas del Cerro, Luís (ed.) |
| |
| | 1998 | 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 | Proceedings Article | |
| | 1998 | 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 | Proceedings Article | |
| 1 |
| Fathi, Madjid (ed.) |
| |
| | 1996 | 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 | Proceedings Article | |
| 1 |
| Fawcett, Tom (ed.) |
| |
| | 2003 | Jaeger, Manfred | | Probabilistic Classifiers and the Concepts they Recognize
In: Proceedings of the Twentieth International Conference on Machine Learning (ICML-03), 266-273 | Proceedings Article | |
| 4 |
| Fehrer, Detlef |
| |
| | 1995 | Fehrer, Detlef | | A unifying logical framework for reason maintenance
Universität des Saarlandes | Thesis - PhD thesis | |
| | 1994 | Fehrer, Detlef | | A Unifying Logical Framework for Reason Maintenance (Deliverable DI.1.2-3P)
In: Medlar II Report PPR2, 47-55 | Proceedings Article | |
| | 1994 | 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 | Proceedings Article | |
| | 1993 | Fehrer, Detlef | | A Unifying Framework for Reason Maintenance
In: Symbolic and Quantitative Approaches to Reasoning and Uncertainty: Proceedings European Conference ECSQARU '93, 113-120 | Proceedings Article | |
| 1 |
| Felleisen, Matthias (ed.) |
| |
| | 2007 | [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 | Proceedings Article | |
| 1 |
| |
| | 2005 | Freiheit, Jörn
[Münch, Susanne]
[Schöttle, Hendrik]
[Sijanski, Grozdana]
[Zangl, Fabrice] | | Enhanced 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 | Proceedings Article | |
| 1 |
| |
| | 2001 | [Fermüller, Christian G.]
[Leitsch, Alexander]
Hustadt, Ullrich
[Tammet, Tanel] | | Resolution Decision Procedures
In: Handbook of Automated Reasoning, 1793-1849 | Part of a Book | |
| 1 |
| Fermüller, Christian (ed.) |
| |
| | 2002 | Sofronie-Stokkermans, Viorica | | On uniform word problems involving bridging operators on distributive lattices
In: Automated Reasoning with Analytic and Related Methods : International Conference, TABLEAUX 2002, 235-250 | Proceedings Article | |
| 2 |
| |
| | 2007 | [Beyer, Dirk]
[Henzinger, Thomas]
[Majumdar, Rupak]
Rybalchenko, Andrey | | Path Invariants
In: PLDI'07 : Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 300-309 | Proceedings Article | |
| | 2007 | [Cook, Byron]
[Podelski, Andreas]
Rybalchenko, Andrey | | Proving Thread Termination
In: PLDI'07 : Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 320-330 | Proceedings Article | |
| 1 |
| Ferreirim, Isabel (ed.) |
| |
| | 1999 | Sofronie-Stokkermans, Viorica | | Priestley representation for distributive lattices with operators and applications to automated theorem proving
In: Dualities, Interpretability and Ordered Structures, 43-54 | Proceedings Article | |
| 1 |
| Fiedler, Herbert (ed.) |
| |
| | 1998 | Weidenbach, Christoph | | Rechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197 | Part of a Book | |
| 1 |
| Filinski, Andrzej (ed.) |
| |
| | 2001 | Ganzinger, Harald | | Bottom-Up Deduction with Deletion and Priorities
In: Programs as Data Objects (PADO-01) : Second Symposium PADO 2001, 276-277 | Proceedings Article | |
| 1 |
| Finkbeiner, Bernd |
| |
| | 2006 | [Dräge, Klaus]
[Finkbeiner, Bernd]
Podelski, Andreas | | Directed Model Checking with Distance-Preserving Abstractions
In: Model checking software : 13th International SPIN Workshop, 19-34 | Proceedings Article | |
| 1 |
| Firozabadhi, Babak Sadighi |
| |
| | 1998 | [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 | Proceedings Article | |
| 2 |
| Fischmann, Matthias |
| |
| | 1999 | Fischmann, Matthias | | On Applications of Decidable Object-Oriented Type Theory
Universität des Saarlandes | Thesis - Masters thesis | |
| | 1997 | [Rahman, Shahid]
[Rückert, Helge]
Fischmann, Matthias | | Dialogues and Ontology, the Dialogical Approach to Free Logic
In: Logique et Analyse [160], 357-374 | Journal Article | |
| 1 |
| |
| | 2003 | Sofronie-Stokkermans, Viorica | | Representation 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 | Part of a Book | |
| 1 |
| |
| | 2005 | [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 | Proceedings Article | |
| 1 |
| |
| | 2002 | [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 | Proceedings Article | |
| 1 |
| |
| | 1999 | 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 | Proceedings Article | |
| 1 |
| |
| | 1993 | Hustadt, Ullrich
Nonnengart, Andreas | | Modalities in Knowledge Representation
In: Proc. of the 6th Australian Joint Conference on Artificial Intelligence (AI '93), 249-254 | Proceedings Article | |
| 1 |
| |
| | 2003 | Kazakov, Yevgeny
de Nivelle, Hans | | Subsumption 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 | Proceedings Article | |
| 3 |
| |
| | 1998 | [Frank, Ian]
Basin, David A. | | Search in Games with Incomplete Information: A Case Study Using Bridge Card Play
In: Artificial Intelligence [100], 87-123 | Journal Article | |
| | 1996 | [Frank, Ian]
Basin, David A. | | Search in Games with Incomplete Information: A Case Study Using Bridge Card Play | Report | |
| | 1992 | 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 | Proceedings Article | |
| 1 |
| |
| | 1998 | Bockmayr, Alexander
Dimopoulos, Yannis | | Mixed Integer Programming Models for Planning Problems
In: Proceedings of the Workshop on Constraint Problem Reformulation (CP-98), 1-6 | Proceedings Article | |
| 7 |
| |
| | 2006 | [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, ??-?? | Proceedings Article | |
| | 2006 | 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 | Journal Article | |
| | 2006 | Freiheit, Jörn
[Zangl, Fabrice] | | Model-based user-interface management for public services
In: 6th European Conference on e-Government, 141-151 | Proceedings Article | |
| | 2006 | [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 | Proceedings Article | |
| | 2005 | [Yuan, Cong]
[Billington, Jonathan]
Freiheit, Jörn | | An 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 | Proceedings Article | |
| | 2005 | Freiheit, Jörn
[Münch, Susanne]
[Schöttle, Hendrik]
[Sijanski, Grozdana]
[Zangl, Fabrice] | | Enhanced 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 | Proceedings Article | |
| | 2005 | [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 | Proceedings Article | |
| 1 |
| |
| | 1996 | 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 | Proceedings Article | |
| 2 |
| |
| | 2001 | 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 | Proceedings Article | |
| | 1994 | 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 | Proceedings Article | |
| 3 |
| Friedrich, Stefan |
| |
| | 1999 | Basin, David A.
Friedrich, Stefan | | Modeling a Hardware Synthesis Methodology in Isabelle
In: Formal Methods in Systems Design [15], 99-122 | Journal Article | |
| | 1998 | Friedrich, Stefan | | Integration of a Decision Procedure for Second-Order Monadic Logic in a Higher-Order Logic Theorem Proving Environment
Universität des Saarlandes | Thesis - Masters thesis | |
| | 1996 | 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 | Proceedings Article | |
| 1 |
| Froideveaux, Christine (ed.) |
| |
| | 1995 | Weydert, Emil | | Numeric 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 | Proceedings Article | |
| 2 |
| Frühwirth, Thom (ed.) |
| |
| | 2004 | [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 | Proceedings Article | |
| | 2004 | 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 | Proceedings Article | |
| 3 |
| |
| | 2006 | 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 | Electronic Proceedings Article | |
| | 2006 | Baumgartner, Peter
Fuchs, Alexander
[Tinelli, Cesare] | | Implementing the Model Evolution Calculus
In: International Journal on Artificial Intelligence Tools [15], 21-52 | Journal Article | |
| | 2004 | 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 | Proceedings Article | |
| 1 |
| |
| | 1996 | Weydert, Emil | | Doxastic Normality Logic: A Qualitative Probabilistic Modal Framework for Defaults and Belief
In: Logic, Action, and Information, 152-171 | Part of a Book | |
| 5 |
| |
| | 2005 | Baumgartner, Peter
[Furbach, Ulrich]
[Yahya, Adnan] | | Automated Reasoning, Knowledge Representation and Management
In: KI - Künstliche Intelligenz [1], 5-11 | Journal Article | |
| | 2005 | 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 | Part of a Book | |
| | 2005 | 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 | Proceedings Article | |
| | 2004 | Baumgartner, Peter
[Furbach, Ulrich]
[Gross-Hardt, Margret]
[Sinner, Alex] | | Living Book -- Deduction, Slicing, and Interaction
In: Journal of Automated Reasoning [32], 259-286 | Journal Article | |
| | 2004 | 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 | Proceedings Article | |
| 8 |
| |
| | 2006 | 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 | Proceedings Article | |
| | 2006 | Sofronie-Stokkermans, Viorica | | Interpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250 | Proceedings Article | |
| | 2000 | | | Deduction | Proceedings | |
| | 2000 | Mukhopadhyay, Supratik
Podelski, Andreas | | Model Checking for Timed Logic Processes
In: Proceedings of the 1st International Conference on Computational Logic, 598-612 | Proceedings Article | |
| | 1998 | 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 | Proceedings Article | |
| | 1998 | 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 | Proceedings Article | |
| | 1997 | Waldmann, Uwe | | A Superposition Calculus for Divisible Torsion-Free Abelian Groups
In: Proceedings of the International Workshop on First-Order Theorem Proving (FTP-97), 130-134 | Proceedings Article | |
| | 1997 | Stuber, Jürgen | | Strong 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 | Proceedings Article | |
| 6 |
| Gabbay, Dov M. |
| |
| | 2001 | 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 | Part of a Book | |
| | 1994 | [Brink, Chris]
Gabbay, Dov M.
Ohlbach, Hans Jürgen | | Towards Automating Duality
In: Journal of Computers and Mathematics with Applications [29], 73-90 | Journal Article | |
| | 1992 | 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 | Proceedings Article | |
| | 1992 | 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 | Proceedings Article | |
| | 1992 | Gabbay, Dov M.
Ohlbach, Hans Jürgen | | Quantifier Elimination in Second-Order Predicate Logic
In: South African Computer Journal [7], 35-43 | Journal Article | |
| | 1991 | Cunningham, J.
Gabbay, Dov M.
Ohlbach, Hans Jürgen | | Towards the MEDLAR Framework
In: ESPRIT '91 Conference Proceedings, 822-841 | Proceedings Article | |
| 5 |
| |
| | 1997 | | | Qualitative and Quantitative Practical Reasoning | Book | |
| | 1994 | Matthews, Seán | | A Theory and its Metatheory in $FS_0$
In: What is a logical system?, 329-354 | Part of a Book | |
| | 1994 | | | Temporal Logic: Proceedings of the 1st International Conference on Temporal Logic | Proceedings | |
| | 1993 | Eisinger, Norbert
Ohlbach, Hans Jürgen | | Deduction Systems Based on Resolution
In: Handbook of Logic in Artificial Intelligence and Logic Programming, 184-271 | Proceedings Article | |
| | 1993 | Plaisted, David A. | | Equational Reasoning and Term Rewriting Systems
In: Handbook of Logic in Artificial Intelligence and Logic Programming, 273-364 | Proceedings Article | |
| 4 |
| |
| | 2002 | Basin, David A.
Matthews, Sean | | Logical Frameworks
In: Handbook of Philosophical Logic, 89-164 | Part of a Book | |
| | 2000 | Weydert, Emil | | Rankings in flux
In: Proceedings of the 3rd International Conference on Formal and Applied Practical Reasoning (FAPR-00), 37-48 | Proceedings Article | |
| | 1997 | Weydert, Emil | | Rational Default Quantifier Logic
In: Proceedings of the 1st International Joint Conference on Qualitative and Quantitative Practical Reasoning (ESQARU-FAPR-97), 589-600 | Proceedings Article | |
| | 1996 | Weydert, Emil | | System J - Revision Entailment: Default Reasoning through Ranking Measure Updates
In: Practical Reasoning - International Conference on Formal and Applied Practical Reasoning, FAPR'96, 637-649 | Proceedings Article | |
| 2 |
| Gaede, Bernd |
| |
| | 1996 | 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 | Proceedings Article | |
| | 1995 | Gaede, Bernd | | Superposition Extended with Sorts
Universität Kaiserslautern | Thesis - Masters thesis | |
| 1 |
| |
| | 1991 | 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 | Proceedings Article | |
| 1 |
| |
| | 2003 | [Gaillourdet, Jean-Marie]
Hillenbrand, Thomas
[Löchner, Bernd]
[Spies, Hendrik] | | The New WALDMEISTER Loop at Work
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 317-321 | Proceedings Article | |
| 1 |
| |
| | 1999 | Delzanno, Giorgio
[Galmiche, Didier]
[Martelli, Maurizio] | | A specification logic for concurrent object-oriented programming
In: Mathematical Structures in Computer Science [9], 253-286 | Journal Article | |
| 1 |
| |
| | 1998 | Delzanno, Giorgio | | Specification of Term Rewriting in Linear Logic
In: Proceedings of Workshop on Proof-Search in Type-Theoretic Languages, ?? | Proceedings Article | |
| 1 |
| |
| | 2001 | Gamkrelidze, Alexander | | Einige Optimierungsmethoden hierarchischer Schaltkreise
Universität des Saarlandes | Thesis - PhD thesis | |
| 1 |
| |
| | 2000 | [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 | Proceedings Article | |
| 58 |
| |
| | 2006 | Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Waldmann, Uwe | | Modular Proof Systems for Partial Functions with Evans Equality
In: Information and Computation [204], 1453-1492 | Journal Article | |
| | 2006 | Ganzinger, Harald
[Korovin, Konstantin] | | Theory Instantiation
In: 13th Conference on Logic for Programming Artificial Intelligence Reasoning (LPAR'06), 497-511 | Proceedings Article | |
| | 2006 | Ganzinger, Harald
[Korovin, Konstantin] | | Theory Instantiation
In: Logic for Programming, Artificial Intelligence, and Reasoning : 13th International Conference, LPAR 2006, 497-511 | Proceedings Article | |
| | 2005 | Ganzinger, Harald
[Stuber, Jürgen] | | Superposition with equivalence reasoning and delayed clause normal form transformation
In: Information and Computation [199], 3-23 | Journal Article | |
| | 2004 | 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 | Proceedings Article | |
| | 2004 | Ganzinger, Harald
[Nieuwenhuis, Robert]
[Nivela, Pilar] | | Fast Term Indexing with Coded Context Trees
In: Journal of Automated Reasoning [32], 103-120 | Journal Article | |
| | 2004 | 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 | Proceedings Article | |
| | 2004 | 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 | Proceedings Article | |
| | 2003 | Ganzinger, Harald
Korovin, Konstantin | | New Directions in Instantiation-Based Theorem Proving
In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), 55-64 | Proceedings Article | |
| | 2003 | Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe | | Superposition modulo a Shostak Theory
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 182-196 | Proceedings Article | |
| | 2003 | Ganzinger, Harald
[Stuber, Jürgen] | | Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 335-349 | Proceedings Article | |
| | 2002 | Ganzinger, Harald
[McAllester, David] | | Logical Algorithms
In: Logic Programming. 18th International Conference, ICLP 2002, 209-223 | Proceedings Article | |
| | 2002 | Ganzinger, Harald | | Shostak Light
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 332-346 | Proceedings Article | |
| | 2001 | Ganzinger, Harald
[McAllester, David] | | A new meta-complexity theorem for bottom-up logic programs
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 514-528 | Proceedings Article | |
| | 2001 | Ganzinger, Harald
Hustadt, Ullrich
Meyer, Christoph
Schmidt, Renate A. | | A Resolution-Based Decision Procedure for Extensions of K4
In: Advances in Modal Logic, Volume 2, 225-246 | Part of a Book | |
| | 2001 | [Basin, David A.]
Ganzinger, Harald | | Automated Complexity Analysis Based on Ordered Resolution
In: Journal of the ACM [48], 70-109 | Journal Article | |
| | 2001 | Ganzinger, Harald | | Bottom-Up Deduction with Deletion and Priorities
In: Programs as Data Objects (PADO-01) : Second Symposium PADO 2001, 276-277 | Proceedings Article | |
| | 2001 | Ganzinger, Harald
[Nieuwenhuis, Robert] | | Constraints and Theorem Proving
In: Contraints in Computational Logics, International Summer School (CCL-99), 159-201 | Proceedings Article | |
| | 2001 | Ganzinger, Harald
[Nieuwenhuis, Robert]
[Nivela, Pilar] | | Context trees
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 242-256 | Proceedings Article | |
| | 2001 | Ganzinger, Harald | | Efficient deductive methods for program analysis
In: ACM SIGPLAN Notices [36], 102-103 | Journal Article | |
| | 2001 | Ganzinger, Harald | | Relating 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 | Proceedings Article | |
| | 2001 | Bachmair, Leo
Ganzinger, Harald | | Resolution Theorem Proving
In: Handbook of Automated Reasoning, 19-99 | Part of a Book | |
| | 2000 | Ganzinger, Harald
Sofronie-Stokkermans, Viorica | | Chaining 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 | Proceedings Article | |
| | 2000 | 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 | Journal Article | |
| | 1999 | Ganzinger, Harald
de Nivelle, Hans | | A 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 | Proceedings Article | |
| | 1999 | 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 | Proceedings Article | |
| | 1999 | 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 | Proceedings Article | |
| | 1998 | 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 | Proceedings Article | |
| | 1998 | Bachmair, Leo
Ganzinger, Harald | | Equational Reasoning in Saturation-Based Theorem Proving
In: Automated Deduction: A Basis for Applications, 353-397 | Part of a Book | |
| | 1998 | [Bachmair, Leo]
Ganzinger, Harald | | Ordered Chaining Calculi for First-Order Theories of Transitive Relations
In: Journal of the ACM [45], 1007-1049 | Journal Article | |
| | 1998 | Ganzinger, Harald | | Preface
In: Theoretical Computer Science [208], 1 | Journal Article | |
| | 1998 | 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 | Proceedings Article | |
| | 1998 | Bachmair, Leo
Ganzinger, Harald | | Strict Basic Superposition
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 160-174 | Proceedings Article | |
| | 1997 | 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 | Proceedings Article | |
| | 1996 | 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 | Proceedings Article | |
| | 1996 | Ganzinger, Harald | | Saturation-based theorem proving (abstract)
In: Automata, Languages and Programming: International Colloquium (ICALP-23), 1-3 | Proceedings Article | |
| | 1996 | 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 | Proceedings Article | |
| | 1995 | Bachmair, Leo
Ganzinger, Harald | | Associative-Commutative Superposition
In: Proceedings of the 4th International Workshop on Conditional and Typed Rewrite Systems (CTRS-94), 1-14 | Proceedings Article | |
| | 1995 | Bachmair, Leo
Ganzinger, Harald
[Lynch, Christopher]
[Snyder, Wayne] | | Basic Paramodulation
In: Information and Computation [121], 172-192 | Journal Article | |
| | 1995 | 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 | Proceedings Article | |
| | 1994 | 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 | Proceedings Article | |
| | 1994 | Bachmair, Leo
Ganzinger, Harald | | Ordered Chaining for Total Orderings
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 435-450 | Proceedings Article | |
| | 1994 | 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 | Journal Article | |
| | 1994 | Bachmair, Leo
Ganzinger, Harald | | Rewrite-based equational theorem proving with selection and simplification
In: Journal of Logic and Computation [4], 217-247 | Journal Article | |
| | 1994 | Bachmair, Leo
Ganzinger, Harald | | Rewrite Techniques for Transitive Relations
In: Proceedings of the 9th IEEE Symposium on Logic in Computer Science, 384-393 | Proceedings Article | |
| | 1994 | Ganzinger, Harald | | The Saturate System | Unpublished/Draft | |
| | 1993 | 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 | Part of a Book | |
| | 1993 | [Bachmair, Leo]
Ganzinger, Harald
Waldmann, Uwe | | Set Constraints are the Monadic Class
In: Eighth Annual IEEE Symposium on Logic in Computer Science, 75-83 | Proceedings Article | |
| | 1993 | [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 | Proceedings Article | |
| | 1992 | 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 | Proceedings Article | |
| | 1992 | 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 | Part of a Book | |
| | 1992 | Bachmair, Leo
Ganzinger, Harald | | Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria
In: Logic Programming and Automated Reasoning, 273-284 | Proceedings Article | |
| | 1992 | 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 | Proceedings Article | |
| | 1992 | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | | Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434 | Proceedings Article | |
| | 1991 | Ganzinger, Harald | | A completion procedure for conditional equations
In: Journal of Symbolic Computation [11], 51-81 | Journal Article | |
| | 1991 | 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 | Proceedings Article | |
| | 1991 | Ganzinger, Harald | | Order-Sorted Completion: The Many-Sorted Way
In: Theoretical Computer Science [89], 3-32 | Journal Article | |
| | 1991 | Bachmair, Leo
Ganzinger, Harald | | Perfect model semantics for logic programs with equality
In: Proceedings International Conference on Logic Programming '91, 645-659 | Proceedings Article | |
| 16 |
| Ganzinger, Harald (ed.) |
| |
| | 2002 | Maier, Patrick | | A Framework for Circular Assume-Guarantee Rules
In: Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, 55-58 | Proceedings Article | |
| | 2002 | Hillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor | | Is Logic Effective for Analyzing C Programs?
In: Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, 27-30 | Proceedings Article | |
| | 2002 | Kazakov, Yevgeny | | Recursive resolution for modal logic
In: Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, 11-15 | Proceedings Article | |
| | 2000 | | | Deduction | Proceedings | |
| | 1999 | Waldmann, Uwe | | Cancellative 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 | Proceedings Article | |
| | 1999 | Hustadt, Ullrich
Schmidt, Renate A. | | Maslov's Class K Revisited
In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 172-186 | Proceedings Article | |
| | 1999 | Sofronie-Stokkermans, Viorica | | On 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 | Proceedings Article | |
| | 1999 | 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 | Proceedings Article | |
| | 1999 | | | Proceedings of the 16th International Conference on Automated Deduction (CADE-16) | Proceedings | |
| | 1999 | | | Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR-99) | Proceedings | |
| | 1999 | 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 | Proceedings Article | |
| | 1999 | Weidenbach, Christoph | | Towards an Automatic Analysis of Security Protocols in First-Order Logic
In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 378-382 | Proceedings Article | |
| | 1996 | Krishna Rao, M. R. K. | | Modularity of termination in term graph rewriting
In: Rewriting Techniques and Applications, 230-244 | Proceedings Article | |
| | 1996 | | | Rewriting Techniques and Applications, 7th International Conference, RTA-96 | Proceedings | |
| | 1996 | Stuber, Jürgen | | Superposition Theorem Proving for Abelian Groups Represented as Integer Modules
In: Rewriting Techniques and Applications, 7th International Conference, RTA-96, 33-47 | Proceedings Article | |
| | 1992 | 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 | Part of a Book | |
| 1 |
| |
| | 2000 | Wu, Jinzhao | | First-Order Polynomial based Theorem Proving
In: Mathematics Mechanizations and Applications, 273-294 | Part of a Book | |
| 1 |
| |
| | 1994 | 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 | Part of a Book | |
| 1 |
| |
| | 2003 | Hoffmann, Jörg
[Geffner, Hector] | | Branching Matters: Alternative Branching in Graphplan
In: 13th International Conference on Automated Planning and Scheduling (ICAPS-13), 22-31 | Proceedings Article | |
| 1 |
| |
| | 1997 | Jaeger, Manfred | | Relational Bayesian Networks
In: Proceedings of the 13th Conference of Uncertainty in Artificial Intelligence (UAI-13), 266-273 | Proceedings Article | |
| 5 |
| |
| | 2005 | [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 | Proceedings Article | |
| | 2005 | [Georgieva, Lilia]
Maier, Patrick | | Description Logics for Shape Analysis
In: Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 321-330 | Proceedings Article | |
| | 2002 | [Georgieva, Lilia]
[Hustadt, Ullrich]
[Schmidt, Renate A.] | | A New Clausal Class Decidable by Hyperresolution | Report | |
| | 2002 | [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 | Proceedings Article | |
| | 2002 | [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 | Proceedings Article | |
| 1 |
| |
| | 2001 | 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 | Proceedings Article | |
| 1 |
| |
| | 1995 | Gerber, Christian | | Entwicklung eines Algorithmus zur effizienten Anfragebeantwortung für eine terminologische Wissensrepräsentationssprache
Universität des Saarlandes | Thesis - Masters thesis | |
| 2 |
| |
| | 2005 | 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 | Proceedings Article | |
| | 1996 | Bockmayr, Alexander
Kasper, Thomas | | Pseudo-Boolean and Finite Domain Constraint Programming: A Case Study
In: Deklarative Constraint Programmierung, 29-41 | Proceedings Article | |
| 1 |
| Ginzburg, Jonathan (ed.) |
| |
| | 1998 | [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 | Proceedings Article | |
| 1 |
| Giua, Alessandro (ed.) |
| |
| | 2006 | Ratschan, Stefan
[Smaus, Jan-Georg] | | Verification-Integrated Falsification of Non-Deterministic Hybrid Systems
In: 2nd IFAC Conference on Analysis and Design of Hybrid Systems, ? | Proceedings Article | |
| 1 |
| Giunchiglia, Enrico (ed.) |
| |
| | 2003 | Hoffmann, Jörg
[Geffner, Hector] | | Branching Matters: Alternative Branching in Graphplan
In: 13th International Conference on Automated Planning and Scheduling (ICAPS-13), 22-31 | Proceedings Article | |
| 1 |
| Giunchiglia, Fausto |
| |
| | 1991 | 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 | Proceedings Article | |
| 1 |
| Giunchiglia, Fausto (ed.) |
| |
| | 1994 | | | Proceedings of the Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems | Report | |
| 1 |
| Gmytrasiewicz, Piotr (ed.) |
| |
| | 2001 | [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 | Proceedings Article | |
| 1 |
| Göbel, Manfred |
| |
| | 2000 | [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 | Proceedings Article | |
| 1 |
| Gomes, Carla |
| |
| | 2006 | 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 | Proceedings Article | |
| 1 |
| Goncharov, Sergey |
| |
| | 2005 | [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 | Journal Article | |
| 1 |
| Gopalakrishnan, Ganesh (ed.) |
| |
| | 2006 | Malkis, Alexander
Podelski, Andreas
Rybalchenko, Andrey | | Thread-Modular Verification and Cartesian Abstraction | Unpublished/Draft | |
| 1 |
| Goranko, Valentin |
| |
| | 2004 | [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 | Proceedings Article | |
| 4 |
| Gordon, Andrew Donald |
| |
| | 2003 | Charatonik, Witold
[Dal Zilio, Silvano]
[Gordon, Andrew Donald]
[Mukhopadhyay, Supratik]
[Talbot, Jean-Marc] | | Model checking mobile ambients
In: Theoretical Computer Science [308], 277-331 | Journal Article | |
| | 2002 | 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 | Proceedings Article | |
| | 2001 | Charatonik, Witold
[Dal Zilio, Silvano]
[Gordon, Andrew Donald]
Mukhopadhyay, Supratik
[Talbot, Jean-Marc] | | The Complexity of Model Checking Mobile Ambients | Report | |
| | 2001 | 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 | Proceedings Article | |
| 2 |
| |
| | 2003 | Maier, Patrick | | Compositional Circular Assume-Guarantee Rules Cannot Be Sound and Complete
In: Foundations of software science and computation structures : 6th International Conference, FOSSACS 2003, 343-357 | Proceedings Article | |
| | 2003 | 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 | Proceedings Article | |
| 5 |
| Goré, Rajeev (ed.) |
| |
| | 2001 | Ganzinger, Harald
[McAllester, David] | | A new meta-complexity theorem for bottom-up logic programs
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 514-528 | Proceedings Article | |
| | 2001 | 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 | Proceedings Article | |
| | 2001 | Ganzinger, Harald
[Nieuwenhuis, Robert]
[Nivela, Pilar] | | Context trees
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 242-256 | Proceedings Article | |
| | 2001 | [Nieuwenhuis, Robert]
Hillenbrand, Thomas
[Riazanov, Alexandre]
[Voronkov, Andrei] | | On the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271 | Proceedings Article | |
| | 2001 | Waldmann, Uwe | | Superposition and Chaining for Totally Ordered Divisible Abelian Groups (Extended Abstract)
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 226-241 | Proceedings Article | |
| 1 |
| Gorny, Peter (ed.) |
| |
| | 1998 | Weidenbach, Christoph | | Rechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197 | Part of a Book | |
| 1 |
| Gotsman, Alexey |
| |
| | 2007 | [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 | Proceedings Article | |
| 3 |
| Gottlob, Georg (ed.) |
| |
| | 2003 | [Thiebaux, Sylvie]
Hoffmann, Jörg
[Nebel, Bernhard] | | In Defense of PDDL Axioms
In: 18th International Joint Conference on Artificial Intelligence, 961-966 | Proceedings Article | |
| | 1999 | Vorobyov, Sergei | | Subtyping Functional+Nonempty Record Types
In: Proceedings of the 12th International Workshop on Computer Science Logic (CSL-98), Annual Conference on the EACSL, 285-297 | Proceedings Article | |
| | 1993 | [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 | Proceedings Article | |
| 1 |
| Gottlob, G. (ed.) |
| |
| | 1997 | 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 | Proceedings Article | |
| 1 |
| Grabowski, Barbara |
| |
| | 2004 | Baumgartner, Peter
[Grabowski, Barbara]
[Oevel, Walter]
[Melis, Erica] | | In2Math - Interaktive Mathematik- und Informatikgrundausbildung
In: Softwaretechnik-Trends [24], 36-45 | Journal Article | |
| 7 |
| Graf, Peter |
| |
| | 1996 | Graf, Peter
Meyer, Christoph | | Advanced indexing operations on substitution trees
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 553-567 | Proceedings Article | |
| | 1996 | Graf, Peter | | Path indexing for AC-theories
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 718-732 | Proceedings Article | |
| | 1996 | Graf, Peter | | Term Indexing | Book | |
| | 1995 | Graf, Peter | | Substitution Tree Indexing
In: Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95), 117-131 | Proceedings Article | |
| | 1995 | Graf, Peter | | Term Indexing
Universität des Saarlandes | Thesis - PhD thesis | |
| | 1994 | Graf, Peter | | Extended Path-Indexing
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 514-528 | Proceedings Article | |
| | 1992 | Graf, Peter | | Unification Using Dynamic Sorts
Universität des Saarlandes | Thesis - Masters thesis | |
| 1 |
| Graf, Susann (ed.) |
| |
| | 2000 | 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 | Proceedings Article | |
