| Title | Author(s) [non member] | Editor(s) [non member] | Year | Type |
| A Combined Superposition and Model Evolution Calculus
In: Journal of Automated Reasoning [47], 191-227 | [Baumgartner, Peter]
Waldmann, Uwe | | 2011 | Journal Article |
| A New Input Technique for Accented Letters in Alphabetical Scripts
In: Proceedings of the 20th International Unicode Conference, C12 | Waldmann, Uwe |  | 2002 | Proceedings Article |
| A New Sorted Logic
In: GWAI-92: Advances in Artificial Inteligence, Proceedings 16th German Workshop on Artificial Intelligence, 43-54 | Weidenbach, Christoph | Ohlbach, Hans Jürgen | 1993 | Proceedings Article |
| A Note on Assumptions about Skolem Functions
In: Journal of Automated Reasoning [15], 267-275 | Ohlbach, Hans Jürgen
Weidenbach, Christoph |  | 1995 | Journal Article |
 | A Phytography of WALDMEISTER
In: AI Communications [15], 127-133 | [Löchner, Bernd]
Hillenbrand, Thomas | | 2002 | Journal Article |
 | A PLTL-prover based on labelled superposition with partial model guidance
In: Automated Reasoning : 6th International Joint Conference, IJCAR 2012, 537-543 | Suda, Martin
Weidenbach, Christoph | [Gramlich, Bernhard]
[Miller, Dale]
[Sattler, Uli] | 2012 | Proceedings Article |
| A Superposition Calculus for Divisible Torsion-Free Abelian Groups
In: Proceedings of the International Workshop on First-Order Theorem Proving (FTP-97), 130-134 | Waldmann, Uwe | [Bonacina, Maria Paola]
[Furbach, Ulrich] | 1997 | Proceedings Article |
 | A Superposition View on Nelson-Oppen
In: Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning, 16-20 | Hillenbrand, Thomas | [Sattler, Ulrike] | 2004 | Electronic Proceedings Article |
 | Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic
Universität des Saarlandes | Bromberger, Martin | | 2012 | Thesis - Bachelor thesis |
| Algebraic and logical methods in automated theorem proving and in the study of concurrency
Universität des Saarlandes | Sofronie-Stokkermans, Viorica |  | 2004 | Thesis - Habilitation thesis |
| Algebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493 | Sofronie-Stokkermans, Viorica | [Iorgulescu, Afrodita]
[Marcus, Solomon]
[Rudeanu, Sergiu]
[Vaida, Dragos] | 2007 | Part of a Book |
| Algorithmic Global Criteria for Excluding Oscillations
In: Bulletin of Mathematical Biology [73], 899-916 | [Weber, Andreas]
Sturm, Thomas
[Abdel-Rahman, Essam O.] |  | 2011 | Journal Article |
| An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
In: Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, 348-362 | [Ludwig, Michel]
Waldmann, Uwe | [Dershowitz, Nachum]
[Voronkov, Andrei] | 2007 | Proceedings Article |
 | Analysis of Authorizations in SAP R/3
Fachhochschule Trier | Lamotte, Manuel |  | 2008 | Thesis - Masters thesis |
 | Analysis of Authorizations in SAP R/3
In: First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving proceedings, 90-104 | Lamotte-Schubert, Manuel
Weidenbach, Christoph | [Peltier, Nicolas]
Sofronie-Stokkermans, Viorica | 2009 | Proceedings Article |
| Analysis of Authorizations in SAP R/3
In: FTP 2009 : First-Order Theorem Proving, 90-104 | Lamotte-Schubert, Manuel
Weidenbach, Christoph | [Peltier, Nicolas]
Sofronie-Stokkermans, Viorica | 2009 | Electronic Proceedings Article |
 | Applications of hierarchical reasoning in the verification of complex systems
In: Electronic Notes in Theoretical Computer Science [174], 39-54 | Jacobs, Swen
Sofronie-Stokkermans, Viorica | | 2007 | Electronic Journal Article |
| Applications of hierarchical reasoning in the verification of complex systems
In: PDPAR'06: Pragmatical Aspects of Decision Procedures in Automated Reasoning, 15-26 | Jacobs, Swen
Sofronie-Stokkermans, Viorica | [Cook, Byron]
[Sebastiani, Roberto] | 2006 | Electronic Proceedings Article |
| Approximate Closed-Form Aggregation of a Fork-Join Structure in Generalised Stochastic Petri Nets
In: Proceedings of the 1st International Conference on Performance Evaluation Methodolgies and Tools, VALUETOOLS 2006, 1-10 | [Lilith, Nimrod]
[Billington, Jonathan]
Freiheit, Jörn | [Lenzini, Luciano]
[Cruz, Rene L.] | 2006 | Electronic Proceedings Article |
| Automated Deduction - CADE-23 : 23rd International Conference on Automated Deduction |  | [Bjørner, Nikolaj]
Sofronie-Stokkermans, Viorica | 2011 | Proceedings |
| Automated Deduction in Geometry : 7th International Workshop, ADG 2008 | | Sturm, Thomas
[Zengler, Christoph] | 2011 | Proceedings |
| Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07) |  | [Ghilardi, Silvio]
[Sattler, Ulrike]
Sofronie-Stokkermans, Viorica
[Tiwari, Ashish] | 2007 | Proceedings |
| Automated Proof Generation of Possibiltiy Properties in Inductive Protocol Verification
Universität des Saarlandes | Neumann, Stephan Rouven | | 2009 | Thesis - Bachelor thesis |
| Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms-
In: Interaction versus Automation : the two Faces of Deduction, 1-33 | Sofronie-Stokkermans, Viorica | [Ball, Thomas]
[Giesl, Jürgen]
[Hähnle, Reiner]
[Nipkow, Tobias] | 2010 | Electronic Proceedings Article |
| Automated reasoning in some local extensions of ordered structures
In: Journal of Multiple-Valued Logic and Soft Computing [13], 397-414 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten | | 2007 | Journal Article |
| Automated reasoning in some local extensions of ordered structures
In: Proceedings of ISMVL 2007, Article1 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten |  | 2007 | Proceedings Article |
 | Automated Theorem Proving by Resolution for Finitely-Valued Logics Based on Distributive Lattices with Operators
In: Multiple-Valued Logic - An International Journal [6], 289-344 | Sofronie-Stokkermans, Viorica | | 2001 | Journal Article |
 | Automated theorem proving by resolution in non-classical logics
In: Annals of Mathematics and Artificial Intelligence [49], 221-252 | Sofronie-Stokkermans, Viorica |  | 2007 | Journal Article |
 | Automated theorem proving by resolution in non-classical logics
In: Fourth International Conference Journees de l'Informatique Messine: Knowledge Discovery and Discrete Mathematics (JIM-03), 151-167 | Sofronie-Stokkermans, Viorica | [Nadif, Mohamed]
[Napoli, Amedeo]
[SanJuan, Eric]
[Sigayret, Alain] | 2003 | Proceedings Article |
 | Automatic Analysis of LAN Infrastructures | Hirth, Simon
Karl, Carsten
Weidenbach, Christoph |  | 2007 | Report |
 | Automatic Analysis of Tree-Based Feature Models with SPASS
Universität des Saarlandes | Dreßler, Christian | | 2009 | Thesis - Masters thesis |
| Automatic Generation of Invariants for Circular Derivations in SUP(LA)
In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, 197-211 | Fietzke, Arnaud
Kruglov, Evgeny
Weidenbach, Christoph | [Bjørner, Nikolaj]
[Voronkov, Andrei] | 2012 | Proceedings Article |
| Automatic Verification of Hybrid Systems with Large Discrete State Space
In: Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, 276-291 | [Damm, Werner]
[Disch, Stefan]
[Hungar, Hardi]
[Pang, Jun]
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | [Graf, Susanne]
[Zhang, Wenhui] | 2006 | Proceedings Article |
| Automatic Verification of Parametric Specifications with Complex Topologies | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | [Bernd, Becker]
[Damm, Werner]
[Fränzle, Martin]
[Olderog, Ernst-Rüdiger]
[Podelski, Andreas]
[Wilhelm, Reinhard] | 2010 | Report |
| Automatic Verification of Parametric Specifications with Complex Topologies
In: Integrated Formal Methods : 8th International Conference, IFM 2010, 152-167 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | [Mery, Dominique]
[Merz, Stephan] | 2010 | Proceedings Article |
| Automatic Verification of the Adequacy of Models for Families of Geometric Objects
In: Automated Deduction in Geometry : 7th International Workshop, ADG 2008, 116-140 | [Lasaruk, Aless]
Sturm, Thomas | Sturm, Thomas
[Zengler, Christoph] | 2011 | Proceedings Article |
 | Automatische Analyse von DHCP und höheren Infrasturkturdiensten mit SPASS
Universität des Saarlandes | Hirth, Simon | | 2006 | Thesis - Masters thesis |
 | Automatische Analyse von Layer 3 Netzwerken mit SPASS
Universität des Saarlandes | Karl, Carsten |  | 2006 | Thesis - Masters thesis |
| Automatisches Beweisen in komplexen Theorien
In: MPG Jahrbuch [-], | Sofronie-Stokkermans, Viorica | | 2006 | Electronic Journal Article |
 | Bitvector Reasoning with SPASS
Universität des Saarlandes | Rusev, Rostislav |  | 2008 | Thesis - Masters thesis |
| Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II)
In: Journal of Symbolic Computation [33], 831-861 | Waldmann, Uwe | | 2002 | Journal Article |
| Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I)
In: Journal of Symbolic Computation [33], 777-829 | Waldmann, Uwe |  | 2002 | Journal Article |
| Cancellative Abelian Monoids in Refutational Theorem Proving
Universität des Saarlandes | Waldmann, Uwe | | 1997 | Thesis - PhD thesis |
| 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 | Waldmann, Uwe | Ganzinger, Harald
[McAllester, David]
[Voronkov, Andrei] | 1999 | Proceedings Article |
 | 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 | Ganzinger, Harald
Sofronie-Stokkermans, Viorica | | 2000 | Proceedings Article |
 | 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 | Hillenbrand, Thomas | [Dahn, Ingo]
[Vigneron, Laurent] | 2003 | Electronic Proceedings Article |
| Combination of Disjoint Theories: Beyond Decidability
In: Proceedings of the 6th International Joint Conference on Automated Reasoning, | [Fontaine, Pascal]
[Merz, Stephan]
Weidenbach, Christoph | | 2012 | Proceedings Article |
| Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation
In: Journal of Symbolic Computation [45-], 261-286 | Tran, Duc-Khanh
[Ringeissen, Christopher]
[Ranise, Silvio]
[Kirchner, Helene] |  | 2009 | Journal Article |
| Combining Superposition, Sorts and Splitting
In: Handbook of Automated Reasoning, 1965-2013 | Weidenbach, Christoph | [Robinson, Alan]
[Voronkov, Andrei] | 2001 | Part of a Book |
| Common Syntax of the DFG-Schwerpunktprogramm ``Deduktion'' | [Hähnle, Reiner]
[Kerber, Manfred]
Weidenbach, Christoph |  | 1996 | Report |
 | Comparing Instance Generation Methods for Automated Reasoning
In: Automated Reasoning with Analytic Tableaux and Related Methods : International Conference, TABLEAUX 2005, 153-168 | Jacobs, Swen
Waldmann, Uwe | [Beckert, Bernhard] | 2005 | Proceedings Article |
 | Comparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78 | Jacobs, Swen
Waldmann, Uwe |  | 2007 | Journal Article |
 | Comparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78 | Jacobs, Swen
Waldmann, Uwe | | 2006 | Electronic Journal Article |
| Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08) |  | [Baader, Franz]
[Ghilardi, Silvio]
[Hermann, Miki]
[Sattler, Ulrike]
Sofronie-Stokkermans, Viorica | 2008 | Proceedings |
| Computational Aspects of a First-Order Logic with Sorts
Universität des Saarlandes | Weidenbach, Christoph | | 1996 | Thesis - PhD thesis |
| Computing small clause normal forms
In: Handbook of Automated Reasoning, 335-367 | Nonnengart, Andreas
Weidenbach, Christoph | [Robinson, Alan]
[Voronkov, Andrei] | 2001 | Part of a Book |
| Constraint Solving for Interpolation | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | [Becker, Bernd]
[Damm, Werner Martin]
[Fränzle, Martin]
[Olderog, Ernst-Rüdiger]
[Podelski, Andreas]
[Wilhelm, Reinhard] | 2009 | Report |
| Constraint Solving for Interpolation
In: Journal of Symbolic Computation [45], 1212-1233 | [Rybalchenko, Andrey]
Sofronie-Stokkermans, Viorica |  | 2010 | Journal Article |
| Constraint Solving for Interpolation
In: Verification, Model Checking and Abstract Interpretation : 8th International Conference, VMCAI 2007, 346-362 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | [Cook, Byron]
[Podelski, Andreas] | 2007 | Proceedings Article |
| Contextual Rewriting | Weidenbach, Christoph
Wischnewski, Patrick |  | 2009 | Report |
| Contextual Rewriting in SPASS
In: PAAR/ESHOL, 115-124 | Weidenbach, Christoph
Wischnewski, Patrick | | 2008 | Proceedings Article |
 | Contextual Rewriting in SPASS
Universität des Saarlandes | Wischnewski, Patrick |  | 2007 | Thesis - Masters thesis |
| Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata
In: HSCC'11 : Proceedings of the 2011 ACM/SIGBED Hybrid Systems: Computation and Control, 73-82 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | [Frazzoli, Emilio]
[Grosu, Radu] | 2011 | Proceedings Article |
| Decidability Results for Saturation-Based Model Building
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 404-420 | Horbach, Matthias
Weidenbach, Christoph | [Schmidt, Renate A.] | 2009 | Proceedings Article |
| Deciding the Inductive Validity of FOR ALL THERE EXISTS* Queries
In: Computer Science Logic : 23rd International Workshop, CSL 2009, 18th Annual Conference of the EACSL, 332-347 | Horbach, Matthias
Weidenbach, Christoph | [Grädel, Erich]
[Kahle, Reinhard] | 2009 | Proceedings Article |
 | Deciding the Inductive Validity of Forall Exists* Queries | Horbach, Matthias
Weidenbach, Christoph |  | 2009 | Report |
| Description Logics for Natural Language Processing
In: International Workshop on Description Logics '94, 80-84 | Fehrer, Detlef
Hustadt, Ullrich
Jaeger, Manfred
Nonnengart, Andreas
Ohlbach, Hans Jürgen
Schmidt, Renate A.
Weidenbach, Christoph
Weydert, Emil | [Baader, Franz]
[Lenzerini, Maurizio]
[Nutt, Werner]
[Patel-Schneider, Peter F.] | 1994 | Proceedings Article |
| Disunification for Ultimately Periodic Interpretations
In: Logic for Programming, Artificial Intelligence, and Reasoning : 16th International Conference, LPAR-16, 290-311 | Horbach, Matthias | [Clarke, Edmund M.]
[Voronkov, Andrei] | 2010 | Proceedings Article |
 | Duality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. Part I
In: Studia Logica [64], 93-132 | Sofronie-Stokkermans, Viorica | | 2000 | Journal Article |
 | Duality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. Part II
In: Studia Logica [64], 151-172 | Sofronie-Stokkermans, Viorica |  | 2000 | Journal Article |
| Efficient Hierarchical Reasoning about Functions over Numerical Domains | Sofronie-Stokkermans, Viorica | [Becker, Bernd]
[Damm, Werner Martin]
[Fränzle, Martin]
[Olderog, Ernst-Rüdiger]
[Podelski, Andreas]
[Wilhelm, Reinhard] | 2008 | Report |
| Efficient hierarchical reasoning about functions over numerical domains
In: KI 2008: Advances in Artificial Intelligence, 135-143 | Sofronie-Stokkermans, Viorica | [Berns, Karsten]
[Breuel, Thomas] | 2008 | Proceedings Article |
 | Efficient Reasoning Procedures for Complex First-Order Theories
Universität des Saarlandes | Wischnewski, Patrick | | 2012 | Thesis - PhD thesis |
| Efficient TBox Subsumption Checking in Combinations of EL and (fragments of) FL0
In: Proceedings of the 2011 International Workshop on Description Logics (DL-2011), 125-135 | Gasse, Francis
Sofronie-Stokkermans, Viorica | [Rosati, Riccardo]
[Rudolph, Sebastian]
[Zakharyaschev, Michael] | 2011 | Electronic Proceedings Article |
| Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
In: Logical Methods in Computer Science [7], 3:1-3:31 | Burel, Guillaume | | 2011 | Electronic Journal Article |
| Embedding Deduction Modulo into a Prover
In: Computer Science Logic : 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, 155-169 | Burel, Guillaume | [Dawar, Anuj]
[Veith, Helmut] | 2010 | Proceedings Article |
| Entscheidbarkeitsprobleme für monadische (Horn)Klauselklassen
Universität des Saarlandes, Naturwissenschaftlich-Technische Fakultät | Weidenbach, Christoph | | 2000 | Thesis - Habilitation thesis |
| Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
In: Science of Computer Programming [77], 1122-1150 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] |  | 2012 | Journal Article |
 | Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces
In: Science of Computer Programming [in press], 1-29 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | 2011 | Electronic Journal Article |
| Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
In: Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, 425-440 | [Damm, Werner]
[Disch, Stefan]
[Hungar, Hardi]
Jacobs, Swen
[Pang, Jun]
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | [Namjoshi, Kedar S.]
[Yoneda, Tomohiro]
[Higashino, Teruo]
[Okamura, Yoshio] | 2007 | Proceedings Article |
| Extending reduction orderings to ACU-compatible reduction orderings
In: Information Processing Letters [67], 43-49 | Waldmann, Uwe | | 1998 | Journal Article |
| Extending the Resolution Method with Sorts
In: Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI '93), 60-65 | Weidenbach, Christoph | Bajcsy, R. | 1993 | Proceedings Article |
| Extensions of the Knuth-Bendix Ordering with LPO-like Properties
Universität des Saarlandes | Ludwig, Michel | | 2006 | Thesis - Masters thesis |
 | External Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288 | Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard | [Mertsching, Bärbel]
[Hund, Marcus]
[Aziz, Zaheer] | 2009 | Proceedings Article |
 | First-Order Atom Definitions Extended
In: Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001), 309-319 | Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph | [Nieuwenhuis, Robert]
[Voronkov, Andrei] | 2001 | Proceedings Article |
 | First-Order Proof Documentation
Universität des Saarlandes | [Dressler, Christian] |  | 2007 | Thesis - Bachelor thesis |
| First-Order Tableaux with Sorts
In: Journal of the Interest Group in Pure and Applied Logics [3], 887-906 | Weidenbach, Christoph | | 1995 | Journal Article |
| First-Order Tableaux with Sorts
In: TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 247-261 | Weidenbach, Christoph | Broda, Krysia
D'Agostino, Marcello
et. al. | 1994 | Proceedings Article |
| First-Order Theorem Proving 2009 | | [Peltier, Nicolas]
Sofronie-Stokkermans, Viorica | 2009 | Proceedings |
| First-Order Theorem Proving : Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09) |  | [Peltier, Nicolas]
Sofronie-Stokkermans, Viorica | 2010 | Electronic Proceedings |
| First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving, Proceedings | | [Peltier, Nicolas]
Sofronie-Stokkermans, Viorica | 2009 | Proceedings |
| First-order theorem proving: Foreword
In: Journal of Symbolic Computation [47], 1009-1010 | [Peltier, Nicolas]
Sofronie-Stokkermans, Viorica |  | 2012 | Journal Article |
 | Formula Renaming with Generalizations
Universität des Saarlandes | Azmy, Noran | | 2012 | Thesis - Masters thesis |
| From Search to Computation: Redundancy Criteria and Simplification at Work
In: Programming Logics, Essays in Memory of Harald Ganzinger, ? | Hillenbrand, Thomas
[Piskac, Ruzica]
Waldmann, Uwe
Weidenbach, Christoph | [Voronkov, Andrei]
Weidenbach, Christoph | 2013 | Part of a Book |
| Frontiers of Combining Systems | | [Tinelli, Cesare]
Sofronie-Stokkermans, Viorica | 2011 | Proceedings |
| Hierarchic Decision Procedures for Verification
Universität des Saarlandes | Jacobs, Swen |  | 2010 | Thesis - PhD thesis |
 | Hierarchic reasoning in local theory extensions
In: Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 219-234 | Sofronie-Stokkermans, Viorica | [Nieuwenhuis, Robert] | 2005 | Proceedings Article |
| Hierarchical and modular reasoning in complex theories: The case of local theory extensions
In: Frontiers of Combining Systems. 6th International Symposium FroCos 2007, Proceedings, 47-71 | Sofronie-Stokkermans, Viorica | [Konev, Boris]
[Wolter, Frank] | 2007 | Proceedings Article |
| Hierarchical and modular reasoning in complex theories: The case of local theory extensions.
In: Proceedings of the Sixth International Workshop on First-Order Theorem Proving (FTP 2007), 1 | Sofronie-Stokkermans, Viorica | [Ranise, Silvio] | 2007 | Proceedings Article |
| Hierarchical reasoning and model generation for the verification of parametric hybrid systems
In: Proceedings of the 24th International Conference on Automated Deduction (CADE-24), 360-376 | Sofronie-Stokkermans, Viorica | [Bonacina, Maria Paola] | 2013 | Proceedings Article |
| Hierarchical Reasoning for the Verification of Parametric Systems
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 171-187 | Sofronie-Stokkermans, Viorica | [Giesl, Jürgen]
[Hähnle, Reiner] | 2010 | Proceedings Article |
 | Incremental Instance Generation in Local Reasoning
In: Computer Aided Verification : 21st International Conference, CAV 2009, 368-382 | Jacobs, Swen | [Bouajjani, Ahmed]
[Maler, Oded] | 2009 | Proceedings Article |
 | Incremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62 | Jacobs, Swen | [Baader, Franz]
[Ghilardi, Silvio]
[Hermann, Miki]
[Sattler, Ulrike]
Sofronie-Stokkermans, Viorica | 2008 | Proceedings Article |
| Integrating incremental flow pipes into a symbolic model checker for hybrid systems | [Damm, Werner]
[Disch, Stefan]
Hagemann, Willem
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | [Becker, Bernd]
[Damm, Werner]
[Finkbeiner, Bernd]
[Fränzle, Martin]
[Olderog, Ernst-Rüdiger]
[Podelski, Andreas] | 2011 | Report |
 | Intelligent Combination of a First Order Theorem Prover and SMT Procedures
Universität des Saarlandes | Zimmer, Stephan | | 2007 | Thesis - other |
| Interpolation in local theory extensions
In: Logical Methods in Computer Science [4], 31 pages | Sofronie-Stokkermans, Viorica |  | 2008 | Electronic Journal Article |
 | Interpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250 | Sofronie-Stokkermans, Viorica | [Furbach, Ulrich]
[Shankar, Natarajan] | 2006 | Proceedings Article |
 | Is Logic Effective for Analyzing C Programs?
In: Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, 27-30 | Hillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor | Charatonik, Witold
Ganzinger, Harald | 2002 | Proceedings Article |
| Labelled Clauses
In: 21st International Conference on Automated Deduction (CADE-21), 311-327 | [Lev-Ami, Tal]
Weidenbach, Christoph
[Reps, Thomas]
[Sagiv, Mooly] | | 2007 | Proceedings Article |
 | Labelled Splitting | Fietzke, Arnaud
Weidenbach, Christoph |  | 2008 | Report |
| Labelled Splitting
In: Annals of Mathematics and Artificial Intelligence [55], 3-34 | Fietzke, Arnaud
Weidenbach, Christoph | | 2009 | Journal Article |
| Labelled Splitting
In: IJCAR, 459-474 | Fietzke, Arnaud
Weidenbach, Christoph |  | 2008 | Proceedings Article |
 | Labelled Splitting
Universität des Saarlandes | Fietzke, Arnaud | | 2007 | Thesis - Masters thesis |
 | Labelled Superposition for PLTL
In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, 391-405 | Suda, Martin
Weidenbach, Christoph | [Bjørner, Nikolaj]
[Voronkov, Andrei] | 2012 | Proceedings Article |
| Lexecute: Visualisation and representation of legal procedures
In: Digital Evidence Journal [3], 17-27 | Freiheit, Jörn
[Luuk, Marc]
[Münch, Susanne]
[Sijanski, Grozdana]
[Zangl, Fabrice] | | 2006 | Journal Article |
| Local reasoning in verification
In: IJCAR'06 Workshop : VERIFY'06: Verification Workshop, 128-145 | Sofronie-Stokkermans, Viorica | [Autexier, Serge]
[Mantel, Heiko] | 2006 | Electronic Proceedings Article |
| Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
In: Deduction and Decision Procedures, 1-22 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Jacobs, Swen | [Baader, Franz]
[Cook, Byron]
[Giesl, Jürgen]
[Nieuwenhuis, Robert] | 2007 | Electronic Proceedings Article |
| Locality and subsumption testing in $\mathcalEL$ and some of its extensions
In: Advances in Modal Logic, Vol.7 (Proceedings of AIML 2008), 315-339 | Sofronie-Stokkermans, Viorica | [Areces, Carlos]
[Goldblatt, Robert] | 2008 | Proceedings Article |
| Locality and subsumption testing in $\mathcalEL$ and some of its extensions
In: Proceedings of the 21st International Workshop on Description Logics (DL-2008), 11pages | Sofronie-Stokkermans, Viorica | [Baader, Franz]
[Lutz, Carsten]
[Motik, Boris] | 2008 | Electronic Proceedings Article |
| Locality results for certain extensions of theories with bridging functions
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 67-83 | Sofronie-Stokkermans, Viorica | [Schmidt, Renate A.] | 2009 | Proceedings Article |
| Maschinell unterstützte Analyse eines Sicherheitsprotokolls
Universität des Saarlandes | Bastuck, Andrea | | 2006 | Thesis - other |
| Model-based user-interface management for public services
In: 6th European Conference on e-Government, 141-151 | Freiheit, Jörn
[Zangl, Fabrice] | [Remenyi, Dan] | 2006 | Proceedings Article |
| Model-based User-interface Management for Public Services
In: Electronic Journal of e-Government [5], 53-62 | Freiheit, Jörn
[Zangl, Fabrice] | | 2007 | Journal Article |
 | Model Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21 | Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph | [Bendisposto, Jens]
[Leuschel, Michael]
[Roggenbach, Markus] | 2010 | Proceedings Article |
 | Modeling Interaction by Sheaves and Geometric Logic
In: Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99), 512-523 | Sofronie-Stokkermans, Viorica
[Stokkermans, Karel] | [Ciobanu, Gabriel]
[Paun, Gheorghe] | 1999 | Proceedings Article |
| Modelling of Cross-Organizational Business Processes
In: Enterprise Modelling and Information Systems Architectures 2007, 87-95 | [Ziemann, Joerg]
[Matheis, Thomas]
Freiheit, Jörn |  | 2007 | Proceedings Article |
| Modelling of Cross-Organizational Business Processes - Current Methods and Standards
In: Enterprise Modelling and Information Systems Architectures [2], 23-31 | [Ziemann, Joerg]
[Matheis, Thomas]
Freiheit, Jörn | | 2007 | Journal Article |
| Modular Proof Systems for Partial Functions with Evans Equality
In: Information and Computation [204], 1453-1492 | Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Waldmann, Uwe |  | 2006 | Journal Article |
| Modular Proof Systems for Partial Functions with Weak Equality
In: Automated reasoning : Second International Joint Conference, IJCAR 2004, 168-182 | Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Waldmann, Uwe | Basin, David
Rusinowitch, Michael | 2004 | Proceedings Article |
| More SPASS with Isabelle : Superposition with Hard Sorts and Configurable Simplification
In: Interactive Theorem Proving : Third International Conference, ITP 2012, 345-360 | [Blanchette, Jasmin Christian]
[Popescu, Andrei]
Wand, Daniel
Weidenbach, Christoph | [Beringer, Lennart]
[Felty, Amy] | 2012 | Proceedings Article |
| Netflow analysis of SAP R/3 traffic in an enterprise
Universität des Saarlandes | Bankstahl, Jan | | 2006 | Thesis - Masters thesis |
 | Netflow analysis of SAP R/3 traffic in an enterprise environment
Universität des Saarlandes | Bankstahl, Jan |  | 2006 | Thesis - other |
 | New Directions in Instantiation-Based Theorem Proving
In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), 55-64 | Ganzinger, Harald
Korovin, Konstantin | [Kolaitis, Phokion] | 2003 | Proceedings Article |
| On combinations of local theory extensions
In: Programming Logics, Essays in Memory of Harald Ganzinger, ? | Sofronie-Stokkermans, Viorica | [Voronkov, Andrei]
Weidenbach, Christoph | 2013 | Part of a Book |
| On Generating Small Clause Normal Forms
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 397-411 | Nonnengart, Andreas
[Rock, Georg]
Weidenbach, Christoph | [Kirchner, Claude]
[Kirchner, Hélène] | 1998 | Proceedings Article |
| On hierarchical reasoning in combinations of theories | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | [Bernd, Becker]
[Damm, Werner]
[Fränzle, Martin]
[Olderog, Ernst-Rüdiger]
[Podelski, Andreas]
[Wilhelm, Reinhard] | 2010 | Report |
| On Hierarchical Reasoning in Combinations of Theories
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 30-45 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | [Giesl, Jürgen]
[Hähnle, Reiner] | 2010 | Proceedings Article |
| On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281 | Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica | [Ramakrishnan, C. R.]
[Rehof, Jakob] | 2008 | Proceedings Article |
 | On the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271 | [Nieuwenhuis, Robert]
Hillenbrand, Thomas
[Riazanov, Alexandre]
[Voronkov, Andrei] | [Goré, Rajeev]
[Leitsch, Alexander]
[Nipkow, Tobias] | 2001 | Proceedings Article |
| On the Saturation of YAGO | Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick |  | 2010 | Report |
| On the Saturation of YAGO
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 441-456 | Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick | [Giesl, Jürgen]
[Hähnle, Reiner] | 2010 | Proceedings Article |
| On the Translation of Timed Automata into First-order Logic
Universität des Saarlandes | Dimova, Dilyana |  | 2009 | Thesis - Masters thesis |
 | 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 | Sofronie-Stokkermans, Viorica | Ganzinger, Harald | 1999 | Proceedings Article |
| On Translation of Finitely-Valued Logics to Classical First-Order Logic
In: Proceedings of the 13th European Conference on Artificial Intelligence (ECAI-98), 410-411 | Sofronie-Stokkermans, Viorica | [Prade, Henri] | 1998 | Proceedings Article |
 | On unification for bounded distributive lattices
In: ACM Transactions on Computational Logic [8], 12.1-12.28 | Sofronie-Stokkermans, Viorica | | 2007 | Journal Article |
 | On unification for bounded distributive lattices
In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), 465-481 | Sofronie-Stokkermans, Viorica | [McAllester, David] | 2000 | Proceedings Article |
| On unification in certain finitely generated varieties of algebras
In: Proceedings of the 21th International Workshop on Unification (UNIF 2007), 1-5 | Sofronie-Stokkermans, Viorica | [Contejean, Evelyne] | 2007 | Electronic Proceedings Article |
 | On uniform word problems involving bridging operators on distributive lattices
In: Automated Reasoning with Analytic and Related Methods : International Conference, TABLEAUX 2002, 235-250 | Sofronie-Stokkermans, Viorica | [Egly, Uwe]
[Fermüller, Christian] | 2002 | Proceedings Article |
 | On Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233 | [Avenhaus, Jürgen]
Hillenbrand, Thomas
[Löchner, Bernd] | | 2003 | Journal Article |
| 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 | Hustadt, Ullrich
Schmidt, Renate A.
Weidenbach, Christoph | [de Swart, Harrie] | 1998 | Proceedings Article |
| Paradigmen und Perspektiven der automatischen Deduktion
In: KI, Organ des Fachbereichs 1 "Künstliche Intelligenz'' der Gesellschaft für Informatik e.V. [4], 15-19 | [Letz, Reinhold]
Weidenbach, Christoph | | 1998 | Journal Article |
| Preface: Special Issue of Selected Extended Papers of CADE-23
In: Journal of Automated Reasoning [?], ?-? | [Bj{\o}rner, Nikolaj]
Sofronie-Stokkermans, Viorica |  | 2013 | Journal Article |
 | Priestley Duality for SHn-algebras and Applications to the Study of Kripke-style Models for SHn-logics
In: Multiple-Valued Logic - An International Journal [5], 281-305 | Sofronie-Stokkermans, Viorica | | 2000 | Journal Article |
| Priestley representation for distributive lattices with operators and applications to automated theorem proving
In: Dualities, Interpretability and Ordered Structures, 43-54 | Sofronie-Stokkermans, Viorica | [Vaz de Carvalho, Júlia]
[Ferreirim, Isabel] | 1999 | Proceedings Article |
 | Propositional Abduction
Universität des Saarlandes | Dimova, Dilyana | | 2007 | Thesis - Bachelor thesis |
| PTIME parametric verification of safety properties for reasonable linear hybrid automata | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | [Bernd, Becker]
[Damm, Werner]
[Fränzle, Martin]
[Olderog, Ernst-Rüdiger]
[Podelski, Andreas]
[Wilhelm, Reinhard] | 2011 | Report |
| PTIME parametric verification of safety properties for reasonable linear hybrid automata
In: Mathematics in Computer Science [5], 469-497 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | 2011 | Journal Article |
 | Real Linear Quantifier Elimination
Universität des Saarlandes | Reuter, Jochen |  | 2013 | Thesis - Masters thesis |
 | Reasoning in Combinations of Theories
Universität des Saarlandes | Ihlemann, Carsten | | 2010 | Thesis - PhD thesis |
| Reasoning in Complex Theories and Applications | Sofronie-Stokkermans, Viorica |  | 2008 | Miscellaneous |
| Reasoning in Complex Theories and Applications. Advanced Lecture
In: ESSLLI 2009 : European Summer School in Logic, Language and Information, 1-64 | Sofronie-Stokkermans, Viorica | | 2009 | Electronic Proceedings Article |
| Rechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197 | Weidenbach, Christoph | [Fiedler, Herbert]
[Gorny, Peter]
[Grass, Werner]
Hölldobler, Steffen
Hotz, Günter
[Kerner, I. O.]
Reischuk, Rüdiger | 1998 | Part of a Book |
| Refutational Theorem Proving for Hierarchic First-Order Theories
In: Applicable Algebra in Engineering, Communication and Computing (AAECC) [5], 193-212 | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | | 1994 | Journal Article |
| 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), ?-? | Sofronie-Stokkermans, Viorica | [Eklund, Patrick]
[Escalada-Imaz, Gonzalo]
[Haehnle, Reiner]
[Vojtas, Peter] | 1998 | Proceedings Article |
| Representation Theorems and Automated Theorem Proving in Non-Classical Logics
In: Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic (ISMVL-99), 242-247 | Sofronie-Stokkermans, Viorica | | 1999 | Proceedings Article |
 | 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 | Sofronie-Stokkermans, Viorica | [Fitting, Melvin]
[Orlowska, Ewa] | 2003 | Part of a Book |
| Representation theorems and the semantics of (semi)lattice-based logics
In: Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logics, 125-134 | Sofronie-Stokkermans, Viorica | | 2001 | Proceedings Article |
| Resolution-based decision procedures for the positive theory of some finitely generated varieties of algebras
In: Proceedings of the 34th International Symposium on Multiple-Valued Logic (ISMVL-2004), 32-37 | Sofronie-Stokkermans, Viorica |  | 2004 | Proceedings Article |
| 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 | Sofronie-Stokkermans, Viorica | [Cachro, Jacek]
[Kijania-Placek, Katarzyna] | 1999 | Proceedings Article |
 | Resolution-based Theorem Proving for SHn-Logics | Sofronie-Stokkermans, Viorica |  | 1998 | Report |
 | Resolution-based theorem proving for SHn-logics
In: Automated Deduction in Classical and Non-Classical Logic (Selected Papers of FTP'98), 268-282 | Sofronie-Stokkermans, Viorica | | 2000 | Proceedings Article |
| Rewrite-based equational theorem proving with selection and simplification
In: Journal of Logic and Computation [4], 217-247 | Bachmair, Leo
Ganzinger, Harald |  | 1994 | Journal Article |
| Satisfiability Checking and Query Answering for large Ontologies
In: PAAR-2012 : Third Workshop on Practical Aspects of Automated Reasoning, 163-177 | Weidenbach, Christoph
Wischnewski, Patrick | | 2012 | Electronic Proceedings Article |
| Semantics of Order-Sorted Specifications
In: Theoretical Computer Science [94], 1-35 | Waldmann, Uwe |  | 1992 | Journal Article |
| Set Constraints are the Monadic Class
In: Eighth Annual IEEE Symposium on Logic in Computer Science, 75-83 | [Bachmair, Leo]
Ganzinger, Harald
Waldmann, Uwe | | 1993 | Proceedings Article |
| Sheaves and geometric logic and applications to modular verification of complex systems | Sofronie-Stokkermans, Viorica | [Becker, Bernd]
[Damm, Werner Martin]
[Fränzle, Martin]
[Olderog, Ernst-Rüdiger]
[Podelski, Andreas]
[Wilhelm, Reinhard] | 2008 | Report |
| Sheaves and geometric logic and applications to modular verification of complex systems
In: Electronic Notes in Theoretical Computer Science [230], 161-187 | Sofronie-Stokkermans, Viorica | | 2009 | Electronic Journal Article |
| Sheaves and geometric logic in concurrency
In: Proceedings of the Eighth Workshop on Geometric and Topological Methods in Concurrency (GETCO 2006), ? | Sofronie-Stokkermans, Viorica |  | 2006 | Proceedings Article |
| SHn-algebras (Symmetric Heyting algebras of order n)
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-11 | [Iturrioz, Luisa]
Sofronie-Stokkermans, Viorica | [Iturrioz, Luisa]
[Orlowska, Ewa]
[Turunen, Esko] | 2000 | Part of a Book |
| SMELS: Satisfiability Modulo Equality with Lazy Superposition
In: Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008, 186-200 | [Lynch, Christopher]
Tran, Duc-Khanh | [Cha, Sungdeok (Steve)]
[Choi, Jin-Young]
[Kim Moonzoo]
[Lee, Insup]
[Viswanathan, Mahesh] | 2008 | Proceedings Article |
| Soft Typing for Ordered Resolution
In: Proceedings of the 14th International Conference on Automated Deduction (CADE-14), 321-335 | Ganzinger, Harald
Meyer, Christoph
Weidenbach, Christoph | [McCune, William] | 1997 | Proceedings Article |
| Some properties of Kleene algebras
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-7 | Sofronie-Stokkermans, Viorica | [Iturrioz, Luisa]
[Orlowska, Ewa]
[Turunen, Esko] | 2000 | Part of a Book |
| Sorted Unification and Its Application to Automated Theorem Proving
In: Proceedings of the CADE-13 Workshop: Term Schematizations and Their Applications, 67-76 | Weidenbach, Christoph | [Hermann, Miki]
[Salzer, Gernot] | 1996 | Proceedings Article |
| Sorted Unification and Tree Automata
In: Automated Deduction - A Basis for Applications, 291-320 | Weidenbach, Christoph | [Bibel, Wolfgang]
[Schmitt, Peter H.] | 1998 | Part of a Book |
| Sorts, Resolution, Tableaux and Propositional Logic
In: KI-94 Workshops: Extended Abstracts, 315-316 | Weidenbach, Christoph | Kunze, Jürgen
Stoyan, Herbert | 1994 | Proceedings Article |
| SPASS V0.77
In: Journal of Automated Reasoning [21], 113-113 | Weidenbach, Christoph
Meyer, Christoph
Cohrs, Christian
Engel, Thorsten
Keen, Enno |  | 1998 | Journal Article |
| SPASS V0.95TPTP
In: Journal of Automated Reasoning [23], 21-21 | Weidenbach, Christoph | | 1999 | Journal Article |
| SPASS Version 0.49
In: Journal of Automated Reasoning [18], 247-252 | Weidenbach, Christoph |  | 1997 | Journal Article |
 | SPASS Version 2.0
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 275-279 | Weidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor | [Voronkov, Andrei] | 2002 | Proceedings Article |
| SPASS Version 3.5
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 140-145 | Weidenbach, Christoph
Dimova, Dilyana
Fietzke, Arnaud
Suda, Martin
Wischnewski, Patrick | [Schmidt, Renate A.] | 2009 | Proceedings Article |
| SPASS & FLOTTER, Version 0.42
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 141-145 | Weidenbach, Christoph
[Gaede, Bernd]
[Rock, Georg] | [McRobbie, M. A.]
[Slaney, J. K.] | 1996 | Proceedings Article |
| SPASS+T
In: ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 18-33 | [Prevosto, Virgile]
Waldmann, Uwe | [Sutcliffe, Geoff]
[Schmidt, Renate]
[Schulz, Stephan] | 2006 | Proceedings Article |
| Special issue on automated deduction: Decidability, complexity, tractability
In: Journal of Symbolic Computation [45], 151-152 | [Ghilardi, Silvio]
[Sattler, Ulrike]
Sofronie-Stokkermans, Viorica
[Tiwari, Ashish] | | 2010 | Journal Article |
| Subterm Contextual Rewriting
In: AI Communications [23], 97-109 | Weidenbach, Christoph
Wischnewski, Patrick |  | 2010 | Journal Article |
| Sudokus as Logical Puzzles
In: Disproving'06: Non-Theorems, Non-Validity, Non-Provability, 2-12 | Hillenbrand, Thomas
Topic, Dalibor
Weidenbach, Christoph | de Nivelle, Hans | 2006 | Proceedings Article |
| Superposition-based Analysis of First-Order Probabilistic Timed Automata
In: Logic for Programming, Artificial Intelligence, and Reasoning : 17th International Conference, LPAR-17, 302-316 | Fietzke, Arnaud
[Hermanns, Holger]
Weidenbach, Christoph | [Fermüller, Christian G.]
[Voronkov, Andrei] | 2010 | Proceedings Article |
| Superposition-based Decision Procedures for Fixed Domain and Minimal Model Semantics
Universität des Saarlandes | Horbach, Matthias | | 2010 | Thesis - PhD thesis |
| Superposition and Chaining for Totally Ordered Divisible Abelian Groups (Extended Abstract)
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 226-241 | Waldmann, Uwe | [Goré, Rajeev]
[Leitsch, Alexander]
[Nipkow, Tobias] | 2001 | Proceedings Article |
 | Superposition and Decision Procedures -- Back and Forth
Universität des Saarlandes | Hillenbrand, Thomas | | 2008 | Thesis - PhD thesis |
| Superposition and Model Evolution Combined
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 17-34 | [Baumgartner, Peter]
Waldmann, Uwe | [Schmidt, Renate A.] | 2009 | Proceedings Article |
| Superposition as a Decision Procedure for Timed Automata
In: Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2011), | Fietzke, Arnaud
Weidenbach, Christoph | [Ratschan, Stefan] | 2011 | Proceedings Article |
| Superposition as a Decision Procedure for Timed Automata
In: Mathematics in Computer Science [6], 409-425 | Fietzke, Arnaud
Weidenbach, Christoph |  | 2012 | Electronic Journal Article |
 | Superposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456 | Kruglov, Evgeny
Weidenbach, Christoph | | 2012 | Journal Article |
 | Superposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456 | Kruglov, Evgeny
Weidenbach, Christoph |  | 2012 | Journal Article |
| Superposition for Bounded Domains
In: Automated Reasoning and Mathematics, Essays in Memory of William W. McCune, 68-100 | Hillenbrand, Thomas
Weidenbach, Christoph | [Bonacina, Maria Paola]
[Stickel, Mark] | 2013 | Part of a Book |
| Superposition for Divisible Torsion-Free Abelian Groups
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 144-159 | Waldmann, Uwe | [Kirchner, Claude]
[Kirchner, Hélène] | 1998 | Proceedings Article |
 | Superposition for Finite Domains | Hillenbrand, Thomas
Weidenbach, Christoph | | 2007 | Report |
 | Superposition for Fixed Domains | Horbach, Matthias
Weidenbach, Christoph |  | 2009 | Report |
| Superposition for Fixed Domains
In: ACM Transactions on Computational Logic [11], 27,1-27,35 | Horbach, Matthias
Weidenbach, Christoph | | 2010 | Journal Article |
| Superposition for Fixed Domains
In: CSL, 293-307 | Horbach, Matthias
Weidenbach, Christoph |  | 2008 | Proceedings Article |
 | Superposition modulo a Shostak Theory
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 182-196 | Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe | [Baader, Franz] | 2003 | Proceedings Article |
| Superposition Modulo Linear Arithmetic
Universität des Saarlandes | Kruglov, Evgeny |  | 2008 | Thesis - Masters thesis |
| Superposition Modulo Linear Arithmetic SUP(LA)
In: Frontiers of Combining Systems : 7th International Symposium, FroCoS 2009, 84-99 | Althaus, Ernst
Kruglov, Evgeny
Weidenbach, Christoph | [Ghilardi, Silvio]
[Sebastiani, Roberto] | 2009 | Proceedings Article |
| 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 | [Bachmair, Leo]
Ganzinger, Harald
Waldmann, Uwe | [Gottlob, Georg]
[Leitsch, Alexander]
[Mundici, Daniele] | 1993 | Proceedings Article |
| SUP(NLA) -- Combining Superposition and Non-Linear Arithmetic
In: 8th International Symposium on Frontiers of Combining Systems, 119-134 | [Eggers, Andreas]
Kruglov, Evgeny
[Kupferschmid, Stefan]
[Scheibler, Karsten]
[Teige, Teige]
Weidenbach, Christoph | Sofronie-Stokkermans, Viorica
[Tinelli, Cesare] | 2011 | Proceedings Article |
| SUP(T) Decides First-Order Logic Fragment Over Ground Theories
In: Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS-4), | Kruglov, Evgeny
Weidenbach, Christoph | [Ratschan, Stefan] | 2011 | Proceedings Article |
| System Description: H-PILoT
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 131-139 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | Schmidt, Renate A. | 2009 | Proceedings Article |
| System Description: H-PILoT (Version 1.9) | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | [Bernd, Becker]
[Damm, Werner]
[Fränzle, Martin]
[Olderog, Ernst-Rüdiger]
[Podelski, Andreas]
[Wilhelm, Reinhard] | 2010 | Report |
| System Description: SPASS Version 1.0.0
In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 314-318 | Weidenbach, Christoph
Afshordel, Bijan
Brahm, Uwe
Cohrs, Christian
Engel, Thorsten
Keen, Enno
Theobalt, Christian
Topić, Dalibor | Ganzinger, Harald | 1999 | Proceedings Article |
 | System Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520 | Weidenbach, Christoph
[Schmidt, Renate]
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor | [Pfenning, Frank] | 2007 | Proceedings Article |
| 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 | Ganzinger, Harald
Waldmann, Uwe | Rusinowitch, M.
Rémy, J.-L. | 1992 | Proceedings Article |
 | The New WALDMEISTER Loop at Work
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 317-321 | [Gaillourdet, Jean-Marie]
Hillenbrand, Thomas
[Löchner, Bernd]
[Spies, Hendrik] | [Baader, Franz] | 2003 | Proceedings Article |
 | The Next WALDMEISTER Loop
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 486-500 | Hillenbrand, Thomas
[Löchner, Bernd] | [Voronkov, Andrei] | 2002 | Proceedings Article |
 | The Next WALDMEISTER Loop (Extended Abstract)
In: Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001, 13-21 | Hillenbrand, Thomas
[Löchner, Bernd] | de Nivelle, Hans
[Schulz, Stephan] | 2001 | Proceedings Article |
| The Saturate System | Ganzinger, Harald | | 1994 | Unpublished/Draft |
| Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434 | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | Kirchner, Hélène
Levi, G. | 1992 | Proceedings Article |
| Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 388-402 | Ganzinger, Harald
Waldmann, Uwe | McRobbie, Michael A.
Slaney, John K. | 1996 | Proceedings Article |
| Theory Instantiation
In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06), 497-511 | Ganzinger, Harald
[Korovin, Konstantin] | [Hermann, Miki]
[Voronkov, Andrei] | 2006 | Proceedings Article |
| 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 | Weidenbach, Christoph | Ganzinger, Harald | 1999 | Proceedings Article |
| Towards Verification of the Pastry Routing Protocol using TLA+
In: Formal Techniques for Distributed Systems : Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011 and 30th IFIP WG 6.1 International Conference, FORTE 2011, 244-258 | Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph | [Bruni, Roberto]
[Dingel, Juergen] | 2011 | Proceedings Article |
| UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings | | [Lynch, Christopher]
[Narendran, Paliath]
[Baader, Franz]
[Ghilardi, Silvio]
[Hermann, Miki]
Sofronie-Stokkermans, Viorica
[Tiwari, Ashish] | 2009 | Electronic Proceedings |
| Unification in Extensions of Shallow Equational Theories
In: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), 76-90 | [Jacquemard, Florent]
Meyer, Christoph
Weidenbach, Christoph | [Nipkow, Tobias] | 1998 | Proceedings Article |
| Unification in Pseudo-Linear Sort Theories is Decidable
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 343-357 | Weidenbach, Christoph | [McRobbie, M. A.]
[Slaney, J. K.] | 1996 | Proceedings Article |
| Unification in Sort Theories
In: Proceedings of the 10th International Workshop on Unification, UNIF'96, 16-25 | Weidenbach, Christoph | [Schulz, Klaus U.]
[Kepser, Stephan] | 1996 | Proceedings Article |
| Unification in Sort Theories and its Applications
In: Annals of Mathematics and Artificial Intelligence [18], 261-293 | Weidenbach, Christoph | | 1996 | Journal Article |
| Using BPEL processes defined by Event-driven Process Chains
In: 5. GI-Workshop "EPK 2006 - Geschäftsprozessmanagement mit Ereignisgesteuerten Prozessketten", 121-135 | [Simon, Carlo]
Freiheit, Jörn
[Olbrich, Sebastian] | [Nüttgens, Markus]
[Rump, Frank J.]
[Mendling, Jan] | 2006 | Proceedings Article |
| Verification and Synthesis Using Real Quantifier Elimination
In: ISSAC 2011 : Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation, 329-336 | Sturm, Thomas
[Tiwari, Ashish] | [Leykin, Anton] | 2011 | Proceedings Article |
| Verifying CSP-OZ-DC specifications with complex data types and timing parameters
In: Proceedings of IFM 2007: Integrated Formal Methods, 233-252 | [Faber, Johannes]
Jacobs, Swen
Sofronie-Stokkermans, Viorica | [Davies, Jim ]
[Gibbons, Jeremy] | 2007 | Proceedings Article |
| Workshop CPL Computational Propositional Logic
In: KI-95 Activities: Workshops, Posters, Demos, 71-72 | Barth, Peter
[Kleine Büning, Hans]
Weidenbach, Christoph | Dreschler-Fischer, Leonie
Pribbenow, Simone | 1995 | Proceedings Article |