| # |  | Year | Author(s) [non member] | | Title | Type | |
|---|
| 1 |
 | Abdel-Rahman, Essam O. |
| |
| | 2011 | [Weber, Andreas]
Sturm, Thomas
[Abdel-Rahman, Essam O.] | | Algorithmic Global Criteria for Excluding Oscillations
In: Bulletin of Mathematical Biology [73], 899-916 | Journal Article | |
| 2 |
| Afshordel, Bijan |
| |
| | 2001 | Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph |  | First-Order Atom Definitions Extended
In: Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001), 309-319 | 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 | |
| 1 |
| |
| | 2009 | Althaus, Ernst
Kruglov, Evgeny
Weidenbach, Christoph | | Superposition Modulo Linear Arithmetic SUP(LA)
In: Frontiers of Combining Systems : 7th International Symposium, FroCoS 2009, 84-99 | Proceedings Article | |
| 1 |
| |
| | 2008 | Sofronie-Stokkermans, Viorica | | Locality and subsumption testing in $\mathcalEL$ and some of its extensions
In: Advances in Modal Logic, Vol.7 (Proceedings of AIML 2008), 315-339 | Proceedings Article | |
| 1 |
| |
| | 2006 | Sofronie-Stokkermans, Viorica | | Local reasoning in verification
In: IJCAR'06 Workshop : VERIFY'06: Verification Workshop, 128-145 | Electronic Proceedings Article | |
| 1 |
| |
| | 2003 | [Avenhaus, Jürgen]
Hillenbrand, Thomas
[Löchner, Bernd] | | On Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233 | Journal Article | |
| 1 |
| |
| | 2009 | Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard | | External Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288 | Proceedings Article | |
| 1 |
| |
| | 2012 | Azmy, Noran | | Formula Renaming with Generalizations
Universität des Saarlandes | Thesis - Masters thesis | |
| 8 |
| |
| | 2009 | | | UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings | Electronic Proceedings | |
| | 2008 | | | Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08) | Proceedings | |
| | 2008 | Jacobs, Swen | | Incremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62 | Proceedings Article | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Locality and subsumption testing in $\mathcalEL$ and some of its extensions
In: Proceedings of the 21st International Workshop on Description Logics (DL-2008), 11pages | Electronic Proceedings Article | |
| | 2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Jacobs, Swen | | Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
In: Deduction and Decision Procedures, 1-22 | Electronic 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 | [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 | |
| | 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 | |
| 5 |
| Bachmair, Leo |
| |
| | 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 | |
| | 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
Waldmann, Uwe | | Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434 | Proceedings Article | |
| 1 |
| Bajcsy, R. (ed.) |
| |
| | 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 | |
| 1 |
| Ball, Thomas (ed.) |
| |
| | 2010 | Sofronie-Stokkermans, Viorica | | 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 | Electronic Proceedings Article | |
| 2 |
| Bankstahl, Jan |
| |
| | 2006 | Bankstahl, Jan | | Netflow analysis of SAP R/3 traffic in an enterprise
Universität des Saarlandes | Thesis - Masters thesis | |
| | 2006 | Bankstahl, Jan | | Netflow analysis of SAP R/3 traffic in an enterprise environment
Universität des Saarlandes | Thesis - other | |
| 1 |
| |
| | 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 | |
| 1 |
| |
| | 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 | |
| 1 |
| |
| | 2006 | Bastuck, Andrea | | Maschinell unterstützte Analyse eines Sicherheitsprotokolls
Universität des Saarlandes | Thesis - other | |
| 2 |
| |
| | 2011 | [Baumgartner, Peter]
Waldmann, Uwe | | A Combined Superposition and Model Evolution Calculus
In: Journal of Automated Reasoning [47], 191-227 | Journal Article | |
| | 2009 | [Baumgartner, Peter]
Waldmann, Uwe | | Superposition and Model Evolution Combined
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 17-34 | Proceedings Article | |
| 1 |
| Beckert, Bernhard (ed.) |
| |
| | 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 | |
| 4 |
| Becker, Bernd (ed.) |
| |
| | 2011 | [Damm, Werner]
[Disch, Stefan]
Hagemann, Willem
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Integrating incremental flow pipes into a symbolic model checker for hybrid systems | Report | |
| | 2009 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation | Report | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Efficient Hierarchical Reasoning about Functions over Numerical Domains | Report | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Sheaves and geometric logic and applications to modular verification of complex systems | Report | |
| 1 |
| |
| | 2010 | Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph | | Model Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21 | Proceedings Article | |
| 1 |
| |
| | 2012 | [Blanchette, Jasmin Christian]
[Popescu, Andrei]
Wand, Daniel
Weidenbach, Christoph | | More SPASS with Isabelle : Superposition with Hard Sorts and Configurable Simplification
In: Interactive Theorem Proving : Third International Conference, ITP 2012, 345-360 | Proceedings Article | |
| 4 |
| |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | PTIME parametric verification of safety properties for reasonable linear hybrid automata | Report | |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies | Report | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | On hierarchical reasoning in combinations of theories | Report | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | System Description: H-PILoT (Version 1.9) | Report | |
| 1 |
| Berns, Karsten (ed.) |
| |
| | 2008 | Sofronie-Stokkermans, Viorica | | Efficient hierarchical reasoning about functions over numerical domains
In: KI 2008: Advances in Artificial Intelligence, 135-143 | Proceedings Article | |
| 1 |
| Bibel, Wolfgang (ed.) |
| |
| | 1998 | Weidenbach, Christoph | | Sorted Unification and Tree Automata
In: Automated Deduction - A Basis for Applications, 291-320 | Part of a Book | |
| 1 |
| Billington, Jonathan |
| |
| | 2006 | [Lilith, Nimrod]
[Billington, Jonathan]
Freiheit, Jörn | | 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 | Electronic Proceedings Article | |
| 1 |
| Bjorner, Nikolaj |
| |
| | 2013 | [Bjorner, Nikolaj]
Sofronie-Stokkermans, Viorica | | Preface: Special Issue of Selected Extended Papers of CADE-23
In: Journal of Automated Reasoning [51], 1-2 | Journal Article | |
| 3 |
| Bjørner, Nikolaj (ed.) |
| |
| | 2012 | Fietzke, Arnaud
Kruglov, Evgeny
Weidenbach, Christoph | | 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 | Proceedings Article | |
| | 2012 | Suda, Martin
Weidenbach, Christoph | | Labelled Superposition for PLTL
In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, 391-405 | Proceedings Article | |
| | 2011 | | | Automated Deduction - CADE-23 : 23rd International Conference on Automated Deduction | Proceedings | |
| 1 |
| Blanchette, Jasmin Christian |
| |
| | 2012 | [Blanchette, Jasmin Christian]
[Popescu, Andrei]
Wand, Daniel
Weidenbach, Christoph | | More SPASS with Isabelle : Superposition with Hard Sorts and Configurable Simplification
In: Interactive Theorem Proving : Third International Conference, ITP 2012, 345-360 | Proceedings Article | |
| 4 |
| Bonacina, Maria Paola (ed.) |
| |
| | 2014 | [Kapur, Deepak]
[Zhang, Zhihai]
Horbach, Matthias
[Zhao, Hantao]
[Lu, Qi]
[Nguyen, ThanhVu] | | Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
In: Automated Reasoning and Mathematics: Essays in Memory of William McCune, 189-228 | Part of a Book | |
| | 2013 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| | 2013 | Hillenbrand, Thomas
Weidenbach, Christoph | | Superposition for Bounded Domains
In: Automated Reasoning and Mathematics, Essays in Memory of William W. McCune, 68-100 | Part of a Book | |
| | 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 | |
| 1 |
| |
| | 2009 | Jacobs, Swen | | Incremental Instance Generation in Local Reasoning
In: Computer Aided Verification : 21st International Conference, CAV 2009, 368-382 | Proceedings Article | |
| 2 |
| |
| | 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 | |
| 1 |
| Breuel, Thomas (ed.) |
| |
| | 2008 | Sofronie-Stokkermans, Viorica | | Efficient hierarchical reasoning about functions over numerical domains
In: KI 2008: Advances in Artificial Intelligence, 135-143 | Proceedings Article | |
| 1 |
| Broda, Krysia (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 |
| Bromberger, Martin |
| |
| | 2012 | Bromberger, Martin | | Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic
Universität des Saarlandes | Thesis - Bachelor thesis | |
| 1 |
| Bruni, Roberto (ed.) |
| |
| | 2011 | Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph | | 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 | Proceedings Article | |
| 1 |
| Bultan, Tevfik (ed.) |
| |
| | 2013 | [Dhungana, Deepak]
Tang, Ching Hoo
Weidenbach, Christoph
[Wischnewski, Patrick] | | Automated Verification of Interactive Rule-Based Configuration Systems
In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 551-561 | Proceedings Article | |
| 2 |
| Burel, Guillaume |
| |
| | 2011 | Burel, Guillaume | | Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
In: Logical Methods in Computer Science [7], 3:1-3:31 | Electronic Journal Article | |
| | 2010 | Burel, Guillaume | | Embedding Deduction Modulo into a Prover
In: Computer Science Logic : 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, 155-169 | Proceedings Article | |
| 1 |
| |
| | 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 | |
| 1 |
| |
| | 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 | |
| 1 |
| Cha, Sungdeok (Steve) (ed.) |
| |
| | 2008 | [Lynch, Christopher]
Tran, Duc-Khanh | | SMELS: Satisfiability Modulo Equality with Lazy Superposition
In: Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008, 186-200 | Proceedings Article | |
| 1 |
| |
| | 2008 | [Lynch, Christopher]
Tran, Duc-Khanh | | SMELS: Satisfiability Modulo Equality with Lazy Superposition
In: Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008, 186-200 | Proceedings Article | |
| 1 |
| Christophe Ringeissen (ed.) |
| |
| | 2013 | [Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas | | Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70 | 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 | |
| 1 |
| |
| | 2010 | Horbach, Matthias | | Disunification for Ultimately Periodic Interpretations
In: Logic for Programming, Artificial Intelligence, and Reasoning : 16th International Conference, LPAR-16, 290-311 | 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 | |
| 1 |
| Contejean, Evelyne (ed.) |
| |
| | 2007 | Sofronie-Stokkermans, Viorica | | On unification in certain finitely generated varieties of algebras
In: Proceedings of the 21th International Workshop on Unification (UNIF 2007), 1-5 | Electronic Proceedings Article | |
| 3 |
| Cook, Byron (ed.) |
| |
| | 2007 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation
In: Verification, Model Checking and Abstract Interpretation : 8th International Conference, VMCAI 2007, 346-362 | Proceedings Article | |
| | 2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Jacobs, Swen | | Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
In: Deduction and Decision Procedures, 1-22 | Electronic 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 |
| Cruz, Rene L. (ed.) |
| |
| | 2006 | [Lilith, Nimrod]
[Billington, Jonathan]
Freiheit, Jörn | | 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 | Electronic 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 |
| Dahn, Ingo (ed.) |
| |
| | 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 | |
| 8 |
| Damm, Werner |
| |
| | 2012 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
In: Science of Computer Programming [77], 1122-1150 | Journal Article | |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| | 2011 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces
In: Science of Computer Programming [in press], 1-29 | Electronic Journal Article | |
| | 2011 | [Damm, Werner]
[Disch, Stefan]
Hagemann, Willem
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Integrating incremental flow pipes into a symbolic model checker for hybrid systems | Report | |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | PTIME parametric verification of safety properties for reasonable linear hybrid automata | Report | |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | PTIME parametric verification of safety properties for reasonable linear hybrid automata
In: Mathematics in Computer Science [5], 469-497 | Journal Article | |
| | 2007 | [Damm, Werner]
[Disch, Stefan]
[Hungar, Hardi]
Jacobs, Swen
[Pang, Jun]
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | 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 | Proceedings Article | |
| | 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 | |
| 3 |
| Damm, Werner Martin (ed.) |
| |
| | 2009 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation | Report | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Efficient Hierarchical Reasoning about Functions over Numerical Domains | Report | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Sheaves and geometric logic and applications to modular verification of complex systems | Report | |
| 5 |
| |
| | 2011 | [Damm, Werner]
[Disch, Stefan]
Hagemann, Willem
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Integrating incremental flow pipes into a symbolic model checker for hybrid systems | Report | |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | PTIME parametric verification of safety properties for reasonable linear hybrid automata | Report | |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies | Report | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | On hierarchical reasoning in combinations of theories | Report | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | System Description: H-PILoT (Version 1.9) | Report | |
| 1 |
| |
| | 2007 | [Faber, Johannes]
Jacobs, Swen
Sofronie-Stokkermans, Viorica | | Verifying CSP-OZ-DC specifications with complex data types and timing parameters
In: Proceedings of IFM 2007: Integrated Formal Methods, 233-252 | Proceedings Article | |
| 1 |
| |
| | 2010 | Burel, Guillaume | | Embedding Deduction Modulo into a Prover
In: Computer Science Logic : 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, 155-169 | Proceedings Article | |
| 1 |
| |
| | 2009 | Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard | | External Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288 | Proceedings Article | |
| 2 |
| |
| | 2006 | Hillenbrand, Thomas
Topic, Dalibor
Weidenbach, Christoph | | Sudokus as Logical Puzzles
In: Disproving'06: Non-Theorems, Non-Validity, Non-Provability, 2-12 | Proceedings Article | |
| | 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 |
| de Swart, Harrie (ed.) |
| |
| | 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 | |
| 1 |
| Denney, Ewen (ed.) |
| |
| | 2013 | [Dhungana, Deepak]
Tang, Ching Hoo
Weidenbach, Christoph
[Wischnewski, Patrick] | | Automated Verification of Interactive Rule-Based Configuration Systems
In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 551-561 | Proceedings Article | |
| 1 |
| Dershowitz, Nachum (ed.) |
| |
| | 2007 | [Ludwig, Michel]
Waldmann, Uwe | | 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 | Proceedings Article | |
| 1 |
| Dhungana, Deepak |
| |
| | 2013 | [Dhungana, Deepak]
Tang, Ching Hoo
Weidenbach, Christoph
[Wischnewski, Patrick] | | Automated Verification of Interactive Rule-Based Configuration Systems
In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 551-561 | Proceedings Article | |
| 2 |
| Dierks, Henning |
| |
| | 2012 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
In: Science of Computer Programming [77], 1122-1150 | Journal Article | |
| | 2011 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces
In: Science of Computer Programming [in press], 1-29 | Electronic Journal Article | |
| 3 |
| |
| | 2009 | Dimova, Dilyana | | On the Translation of Timed Automata into First-order Logic
Universität des Saarlandes | Thesis - Masters thesis | |
| | 2009 | Weidenbach, Christoph
Dimova, Dilyana
Fietzke, Arnaud
Suda, Martin
Wischnewski, Patrick | | SPASS Version 3.5
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 140-145 | Proceedings Article | |
| | 2007 | Dimova, Dilyana | | Propositional Abduction
Universität des Saarlandes | Thesis - Bachelor thesis | |
| 1 |
| |
| | 2011 | Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph | | 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 | Proceedings Article | |
| 5 |
| |
| | 2012 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
In: Science of Computer Programming [77], 1122-1150 | Journal Article | |
| | 2011 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces
In: Science of Computer Programming [in press], 1-29 | Electronic Journal Article | |
| | 2011 | [Damm, Werner]
[Disch, Stefan]
Hagemann, Willem
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Integrating incremental flow pipes into a symbolic model checker for hybrid systems | Report | |
| | 2007 | [Damm, Werner]
[Disch, Stefan]
[Hungar, Hardi]
Jacobs, Swen
[Pang, Jun]
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | 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 | Proceedings Article | |
| | 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 | |
| 1 |
| 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 | |
| 1 |
| |
| | 2007 | [Dressler, Christian] | | First-Order Proof Documentation
Universität des Saarlandes | Thesis - Bachelor thesis | |
| 1 |
| |
| | 2009 | Dreßler, Christian | | Automatic Analysis of Tree-Based Feature Models with SPASS
Universität des Saarlandes | Thesis - Masters thesis | |
| 1 |
| |
| | 2011 | [Eggers, Andreas]
Kruglov, Evgeny
[Kupferschmid, Stefan]
[Scheibler, Karsten]
[Teige, Teige]
Weidenbach, Christoph | | SUP(NLA) -- Combining Superposition and Non-Linear Arithmetic
In: 8th International Symposium on Frontiers of Combining Systems, 119-134 | Proceedings Article | |
| 1 |
| |
| | 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 | |
| 1 |
| |
| | 2013 | [Errami, H.]
[Eiswirth, M.]
[Grigoriev. D.]
[Seiler, W.]
Sturm, T.
[Weber, A.] | | Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates
In: Proceedings of the CASC 2013, 88-99 | Proceedings Article | |
| 1 |
| |
| | 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 |
| |
| | 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 | |
| 1 |
| Errami, H. |
| |
| | 2013 | [Errami, H.]
[Eiswirth, M.]
[Grigoriev. D.]
[Seiler, W.]
Sturm, T.
[Weber, A.] | | Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates
In: Proceedings of the CASC 2013, 88-99 | Proceedings Article | |
| 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 | |
| 1 |
| Esquivel Pinto, Claudia So fia |
| |
| | 2013 | Esquivel Pinto, Claudia So fia | | Computing Variable Orders for SAT-Problems
Universität des Saarlandes | Thesis - Masters thesis | |
| 1 |
| et. al. (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 | |
| 3 |
| Faber, Johannes |
| |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies | Report | |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies
In: Integrated Formal Methods : 8th International Conference, IFM 2010, 152-167 | Proceedings Article | |
| | 2007 | [Faber, Johannes]
Jacobs, Swen
Sofronie-Stokkermans, Viorica | | Verifying CSP-OZ-DC specifications with complex data types and timing parameters
In: Proceedings of IFM 2007: Integrated Formal Methods, 233-252 | Proceedings Article | |
| 1 |
| Fehrer, Detlef |
| |
| | 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 | |
| 1 |
| Felty, Amy (ed.) |
| |
| | 2012 | [Blanchette, Jasmin Christian]
[Popescu, Andrei]
Wand, Daniel
Weidenbach, Christoph | | More SPASS with Isabelle : Superposition with Hard Sorts and Configurable Simplification
In: Interactive Theorem Proving : Third International Conference, ITP 2012, 345-360 | Proceedings Article | |
| 1 |
| Fermüller, Christian G. (ed.) |
| |
| | 2010 | Fietzke, Arnaud
[Hermanns, Holger]
Weidenbach, Christoph | | Superposition-based Analysis of First-Order Probabilistic Timed Automata
In: Logic for Programming, Artificial Intelligence, and Reasoning : 17th International Conference, LPAR-17, 302-316 | Proceedings Article | |
| 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 | |
| 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 | |
| 9 |
| Fietzke, Arnaud |
| |
| | 2012 | Fietzke, Arnaud
Kruglov, Evgeny
Weidenbach, Christoph | | 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 | Proceedings Article | |
| | 2012 | Fietzke, Arnaud
Weidenbach, Christoph | | Superposition as a Decision Procedure for Timed Automata
In: Mathematics in Computer Science [6], 409-425 | Electronic Journal Article | |
| | 2011 | Fietzke, Arnaud
Weidenbach, Christoph | | Superposition as a Decision Procedure for Timed Automata
In: Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2011), | Proceedings Article | |
| | 2010 | Fietzke, Arnaud
[Hermanns, Holger]
Weidenbach, Christoph | | Superposition-based Analysis of First-Order Probabilistic Timed Automata
In: Logic for Programming, Artificial Intelligence, and Reasoning : 17th International Conference, LPAR-17, 302-316 | Proceedings Article | |
| | 2009 | Fietzke, Arnaud
Weidenbach, Christoph | | Labelled Splitting
In: Annals of Mathematics and Artificial Intelligence [55], 3-34 | Journal Article | |
| | 2009 | Weidenbach, Christoph
Dimova, Dilyana
Fietzke, Arnaud
Suda, Martin
Wischnewski, Patrick | | SPASS Version 3.5
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 140-145 | Proceedings Article | |
| | 2008 | Fietzke, Arnaud
Weidenbach, Christoph | | Labelled Splitting | Report | |
| | 2008 | Fietzke, Arnaud
Weidenbach, Christoph | | Labelled Splitting
In: IJCAR, 459-474 | Proceedings Article | |
| | 2007 | Fietzke, Arnaud | | Labelled Splitting
Universität des Saarlandes | Thesis - Masters thesis | |
| 1 |
| Finkbeiner, Bernd (ed.) |
| |
| | 2011 | [Damm, Werner]
[Disch, Stefan]
Hagemann, Willem
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Integrating incremental flow pipes into a symbolic model checker for hybrid systems | Report | |
| 1 |
| Fitting, Melvin (ed.) |
| |
| | 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 |
| Fontaine, Pascal |
| |
| | 2012 | [Fontaine, Pascal]
[Merz, Stephan]
Weidenbach, Christoph | | Combination of Disjoint Theories: Beyond Decidability
In: Proceedings of the 6th International Joint Conference on Automated Reasoning, | Proceedings Article | |
| 1 |
| Fontaine, Pascal (ed.) |
| |
| | 2013 | Horbach, Matthias
Sofronie-Stokkermans, Viorica | | Obtaining Finite Local Theory Axiomatizations via Saturation
In: Frontiers of Combining Systems - 9th International Symposium, 198-213 | Proceedings Article | |
| 8 |
| Fränzle, Martin (ed.) |
| |
| | 2011 | [Damm, Werner]
[Disch, Stefan]
Hagemann, Willem
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Integrating incremental flow pipes into a symbolic model checker for hybrid systems | Report | |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | PTIME parametric verification of safety properties for reasonable linear hybrid automata | Report | |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies | Report | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | On hierarchical reasoning in combinations of theories | Report | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | System Description: H-PILoT (Version 1.9) | Report | |
| | 2009 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation | Report | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Efficient Hierarchical Reasoning about Functions over Numerical Domains | Report | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Sheaves and geometric logic and applications to modular verification of complex systems | Report | |
| 1 |
| |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| 7 |
| |
| | 2007 | Freiheit, Jörn
[Zangl, Fabrice] | | Model-based User-interface Management for Public Services
In: Electronic Journal of e-Government [5], 53-62 | Journal Article | |
| | 2007 | [Ziemann, Joerg]
[Matheis, Thomas]
Freiheit, Jörn | | Modelling of Cross-Organizational Business Processes
In: Enterprise Modelling and Information Systems Architectures 2007, 87-95 | Proceedings Article | |
| | 2007 | [Ziemann, Joerg]
[Matheis, Thomas]
Freiheit, Jörn | | Modelling of Cross-Organizational Business Processes - Current Methods and Standards
In: Enterprise Modelling and Information Systems Architectures [2], 23-31 | Journal Article | |
| | 2006 | [Lilith, Nimrod]
[Billington, Jonathan]
Freiheit, Jörn | | 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 | Electronic 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 | |
| 2 |
| |
| | 2006 | Sofronie-Stokkermans, Viorica | | Interpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250 | 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 | |
| 1 |
| 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 | |
| 1 |
| Gaillourdet, Jean-Marie |
| |
| | 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 | |
| 15 |
| Ganzinger, Harald |
| |
| | 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: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06), 497-511 | 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 | |
| | 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 | |
| | 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 | 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 | |
| | 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 | Ganzinger, Harald | | The Saturate System | Unpublished/Draft | |
| | 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 | 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 | |
| 5 |
| Ganzinger, Harald (ed.) |
| |
| | 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 | |
| | 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 | 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 | 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 | |
| 1 |
| Gasse, Francis |
| |
| | 2011 | Gasse, Francis
Sofronie-Stokkermans, Viorica | | 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 | Electronic Proceedings Article | |
| 1 |
| Ghilardi, Silvio |
| |
| | 2010 | [Ghilardi, Silvio]
[Sattler, Ulrike]
Sofronie-Stokkermans, Viorica
[Tiwari, Ashish] | | Special issue on automated deduction: Decidability, complexity, tractability
In: Journal of Symbolic Computation [45], 151-152 | Journal Article | |
| 5 |
| Ghilardi, Silvio (ed.) |
| |
| | 2009 | Althaus, Ernst
Kruglov, Evgeny
Weidenbach, Christoph | | Superposition Modulo Linear Arithmetic SUP(LA)
In: Frontiers of Combining Systems : 7th International Symposium, FroCoS 2009, 84-99 | Proceedings Article | |
| | 2009 | | | UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings | Electronic Proceedings | |
| | 2008 | | | Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08) | Proceedings | |
| | 2008 | Jacobs, Swen | | Incremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62 | Proceedings Article | |
| | 2007 | | | Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07) | Proceedings | |
| 1 |
| Gibbons, Jeremy (ed.) |
| |
| | 2007 | [Faber, Johannes]
Jacobs, Swen
Sofronie-Stokkermans, Viorica | | Verifying CSP-OZ-DC specifications with complex data types and timing parameters
In: Proceedings of IFM 2007: Integrated Formal Methods, 233-252 | Proceedings Article | |
| 5 |
| Giesl, Jürgen (ed.) |
| |
| | 2010 | Sofronie-Stokkermans, Viorica | | 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 | Electronic Proceedings Article | |
| | 2010 | Sofronie-Stokkermans, Viorica | | Hierarchical Reasoning for the Verification of Parametric Systems
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 171-187 | Proceedings Article | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | On Hierarchical Reasoning in Combinations of Theories
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 30-45 | Proceedings Article | |
| | 2010 | Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick | | On the Saturation of YAGO
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 441-456 | Proceedings Article | |
| | 2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Jacobs, Swen | | Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
In: Deduction and Decision Procedures, 1-22 | Electronic Proceedings Article | |
| 1 |
| Goldblatt, Robert (ed.) |
| |
| | 2008 | Sofronie-Stokkermans, Viorica | | Locality and subsumption testing in $\mathcalEL$ and some of its extensions
In: Advances in Modal Logic, Vol.7 (Proceedings of AIML 2008), 315-339 | Proceedings Article | |
| 2 |
| Goré, Rajeev (ed.) |
| |
| | 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 |
| |
| | 1998 | Weidenbach, Christoph | | Rechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197 | Part of a Book | |
| 1 |
| |
| | 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 |
| |
| | 2009 | Horbach, Matthias
Weidenbach, Christoph | | 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 | Proceedings Article | |
| 1 |
| |
| | 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 | |
| 1 |
| |
| | 2012 | Suda, Martin
Weidenbach, Christoph | | A PLTL-prover based on labelled superposition with partial model guidance
In: Automated Reasoning : 6th International Joint Conference, IJCAR 2012, 537-543 | Proceedings Article | |
| 1 |
| |
| | 1998 | Weidenbach, Christoph | | Rechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197 | Part of a Book | |
| 1 |
| |
| | 2013 | [Errami, H.]
[Eiswirth, M.]
[Grigoriev. D.]
[Seiler, W.]
Sturm, T.
[Weber, A.] | | Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates
In: Proceedings of the CASC 2013, 88-99 | Proceedings Article | |
| 1 |
| |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| 1 |
| |
| | 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 | |
| 3 |
| |
| | 2012 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
In: Science of Computer Programming [77], 1122-1150 | Journal Article | |
| | 2011 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces
In: Science of Computer Programming [in press], 1-29 | Electronic Journal Article | |
| | 2011 | [Damm, Werner]
[Disch, Stefan]
Hagemann, Willem
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Integrating incremental flow pipes into a symbolic model checker for hybrid systems | Report | |
| 1 |
| |
| | 1996 | [Hähnle, Reiner]
[Kerber, Manfred]
Weidenbach, Christoph | | Common Syntax of the DFG-Schwerpunktprogramm ``Deduktion'' | Report | |
| 4 |
| |
| | 2010 | Sofronie-Stokkermans, Viorica | | 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 | Electronic Proceedings Article | |
| | 2010 | Sofronie-Stokkermans, Viorica | | Hierarchical Reasoning for the Verification of Parametric Systems
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 171-187 | Proceedings Article | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | On Hierarchical Reasoning in Combinations of Theories
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 30-45 | Proceedings Article | |
| | 2010 | Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick | | On the Saturation of YAGO
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 441-456 | Proceedings Article | |
| 1 |
| Hermanns, Holger |
| |
| | 2010 | Fietzke, Arnaud
[Hermanns, Holger]
Weidenbach, Christoph | | Superposition-based Analysis of First-Order Probabilistic Timed Automata
In: Logic for Programming, Artificial Intelligence, and Reasoning : 17th International Conference, LPAR-17, 302-316 | Proceedings Article | |
| 5 |
| Hermann, Miki (ed.) |
| |
| | 2009 | | | UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings | Electronic Proceedings | |
| | 2008 | | | Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08) | Proceedings | |
| | 2008 | Jacobs, Swen | | Incremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62 | Proceedings Article | |
| | 2006 | Ganzinger, Harald
[Korovin, Konstantin] | | Theory Instantiation
In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06), 497-511 | Proceedings Article | |
| | 1996 | Weidenbach, Christoph | | Sorted Unification and Its Application to Automated Theorem Proving
In: Proceedings of the CADE-13 Workshop: Term Schematizations and Their Applications, 67-76 | Proceedings Article | |
| 1 |
| Higashino, Teruo (ed.) |
| |
| | 2007 | [Damm, Werner]
[Disch, Stefan]
[Hungar, Hardi]
Jacobs, Swen
[Pang, Jun]
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | 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 | Proceedings Article | |
| 18 |
| Hillenbrand, Thomas |
| |
| | 2013 | Hillenbrand, Thomas
[Piskac, Ruzica]
Waldmann, Uwe
Weidenbach, Christoph | | From Search to Computation: Redundancy Criteria and Simplification at Work
In: Programming Logics, Essays in Memory of Harald Ganzinger, ? | Part of a Book | |
| | 2013 | Hillenbrand, Thomas
Weidenbach, Christoph | | Superposition for Bounded Domains
In: Automated Reasoning and Mathematics, Essays in Memory of William W. McCune, 68-100 | Part of a Book | |
| | 2008 | Hillenbrand, Thomas | | Superposition and Decision Procedures -- Back and Forth
Universität des Saarlandes | Thesis - PhD thesis | |
| | 2007 | Hillenbrand, Thomas
Weidenbach, Christoph | | Superposition for Finite Domains | Report | |
| | 2007 | Weidenbach, Christoph
[Schmidt, Renate]
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor | | System Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520 | Proceedings Article | |
| | 2006 | Hillenbrand, Thomas
Topic, Dalibor
Weidenbach, Christoph | | Sudokus as Logical Puzzles
In: Disproving'06: Non-Theorems, Non-Validity, Non-Provability, 2-12 | Proceedings Article | |
| | 2004 | Hillenbrand, Thomas | | A Superposition View on Nelson-Oppen
In: Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning, 16-20 | Electronic Proceedings Article | |
| | 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 | |
| | 2003 | [Avenhaus, Jürgen]
Hillenbrand, Thomas
[Löchner, Bernd] | | On Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233 | Journal 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 | [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 | |
| | 2002 | [Löchner, Bernd]
Hillenbrand, Thomas | | A Phytography of WALDMEISTER
In: AI Communications [15], 127-133 | Journal 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 | 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 | |
| | 2002 | Hillenbrand, Thomas
[Löchner, Bernd] | | The Next WALDMEISTER Loop
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 486-500 | Proceedings Article | |
| | 2001 | Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph | | First-Order Atom Definitions Extended
In: Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001), 309-319 | 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 | 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 | |
| 2 |
| |
| | 2007 | Hirth, Simon
Karl, Carsten
Weidenbach, Christoph | | Automatic Analysis of LAN Infrastructures | Report | |
| | 2006 | Hirth, Simon | | Automatische Analyse von DHCP und höheren Infrasturkturdiensten mit SPASS
Universität des Saarlandes | Thesis - Masters thesis | |
| 1 |
| Hölldobler, Steffen (ed.) |
| |
| | 1998 | Weidenbach, Christoph | | Rechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197 | Part of a Book | |
| 11 |
| Horbach, Matthias |
| |
| | 2014 | [Kapur, Deepak]
[Zhang, Zhihai]
Horbach, Matthias
[Zhao, Hantao]
[Lu, Qi]
[Nguyen, ThanhVu] | | Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
In: Automated Reasoning and Mathematics: Essays in Memory of William McCune, 189-228 | Part of a Book | |
| | 2013 | Horbach, Matthias | | INFORMATIK 2013 - Informatik angepasst an Mensch, Organisation und Umwelt | Book | |
| | 2013 | Horbach, Matthias
Sofronie-Stokkermans, Viorica | | Obtaining Finite Local Theory Axiomatizations via Saturation
In: Frontiers of Combining Systems - 9th International Symposium, 198-213 | Proceedings Article | |
| | 2010 | Horbach, Matthias | | Disunification for Ultimately Periodic Interpretations
In: Logic for Programming, Artificial Intelligence, and Reasoning : 16th International Conference, LPAR-16, 290-311 | Proceedings Article | |
| | 2010 | Horbach, Matthias | | Superposition-based Decision Procedures for Fixed Domain and Minimal Model Semantics
Universität des Saarlandes | Thesis - PhD thesis | |
| | 2010 | Horbach, Matthias
Weidenbach, Christoph | | Superposition for Fixed Domains
In: ACM Transactions on Computational Logic [11], 27,1-27,35 | Journal Article | |
| | 2009 | Horbach, Matthias
Weidenbach, Christoph | | Decidability Results for Saturation-Based Model Building
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 404-420 | Proceedings Article | |
| | 2009 | Horbach, Matthias
Weidenbach, Christoph | | 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 | Proceedings Article | |
| | 2009 | Horbach, Matthias
Weidenbach, Christoph | | Deciding the Inductive Validity of Forall Exists* Queries | Report | |
| | 2009 | Horbach, Matthias
Weidenbach, Christoph | | Superposition for Fixed Domains | Report | |
| | 2008 | Horbach, Matthias
Weidenbach, Christoph | | Superposition for Fixed Domains
In: CSL, 293-307 | Proceedings Article | |
| 1 |
| Horbach, Matthias (ed.) |
| |
| | 2013 | Horbach, Matthias | | INFORMATIK 2013 - Informatik angepasst an Mensch, Organisation und Umwelt | Book | |
| 1 |
| Hotz, Günter (ed.) |
| |
| | 1998 | Weidenbach, Christoph | | Rechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197 | Part of a Book | |
| 1 |
| Hund, Marcus (ed.) |
| |
| | 2009 | Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard | | External Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288 | Proceedings Article | |
| 2 |
| Hungar, Hardi |
| |
| | 2007 | [Damm, Werner]
[Disch, Stefan]
[Hungar, Hardi]
Jacobs, Swen
[Pang, Jun]
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | 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 | Proceedings Article | |
| | 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 |
| |
| | 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 | |
| | 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 | |
| 14 |
| Ihlemann, Carsten |
| |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | PTIME parametric verification of safety properties for reasonable linear hybrid automata | Report | |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | PTIME parametric verification of safety properties for reasonable linear hybrid automata
In: Mathematics in Computer Science [5], 469-497 | Journal Article | |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies | Report | |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies
In: Integrated Formal Methods : 8th International Conference, IFM 2010, 152-167 | Proceedings Article | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | On hierarchical reasoning in combinations of theories | Report | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | On Hierarchical Reasoning in Combinations of Theories
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 30-45 | Proceedings Article | |
| | 2010 | Ihlemann, Carsten | | Reasoning in Combinations of Theories
Universität des Saarlandes | Thesis - PhD thesis | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | System Description: H-PILoT (Version 1.9) | Report | |
| | 2009 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | System Description: H-PILoT
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 131-139 | Proceedings Article | |
| | 2008 | Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica | | On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281 | Proceedings Article | |
| | 2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten | | Automated reasoning in some local extensions of ordered structures
In: Journal of Multiple-Valued Logic and Soft Computing [13], 397-414 | Journal Article | |
| | 2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten | | Automated reasoning in some local extensions of ordered structures
In: Proceedings of ISMVL 2007, Article1 | Proceedings Article | |
| | 2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Jacobs, Swen | | Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
In: Deduction and Decision Procedures, 1-22 | Electronic Proceedings Article | |
| 1 |
| Iorgulescu, Afrodita (ed.) |
| |
| | 2007 | Sofronie-Stokkermans, Viorica | | Algebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493 | Part of a Book | |
| 1 |
| |
| | 2000 | [Iturrioz, Luisa]
Sofronie-Stokkermans, Viorica | | SHn-algebras (Symmetric Heyting algebras of order n)
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-11 | Part of a Book | |
| 2 |
| |
| | 2000 | [Iturrioz, Luisa]
Sofronie-Stokkermans, Viorica | | SHn-algebras (Symmetric Heyting algebras of order n)
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-11 | Part of a Book | |
| | 2000 | Sofronie-Stokkermans, Viorica | | Some properties of Kleene algebras
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-7 | Part of a Book | |
| 14 |
| Jacobs, Swen |
| |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies | Report | |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies
In: Integrated Formal Methods : 8th International Conference, IFM 2010, 152-167 | Proceedings Article | |
| | 2010 | Jacobs, Swen | | Hierarchic Decision Procedures for Verification
Universität des Saarlandes | Thesis - PhD thesis | |
| | 2009 | Jacobs, Swen | | Incremental Instance Generation in Local Reasoning
In: Computer Aided Verification : 21st International Conference, CAV 2009, 368-382 | Proceedings Article | |
| | 2008 | Jacobs, Swen | | Incremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62 | Proceedings Article | |
| | 2008 | Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica | | On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281 | Proceedings Article | |
| | 2007 | Jacobs, Swen
Sofronie-Stokkermans, Viorica | | Applications of hierarchical reasoning in the verification of complex systems
In: Electronic Notes in Theoretical Computer Science [174], 39-54 | Electronic Journal Article | |
| | 2007 | Jacobs, Swen
Waldmann, Uwe | | Comparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78 | Journal Article | |
| | 2007 | [Damm, Werner]
[Disch, Stefan]
[Hungar, Hardi]
Jacobs, Swen
[Pang, Jun]
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | 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 | Proceedings Article | |
| | 2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Jacobs, Swen | | Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
In: Deduction and Decision Procedures, 1-22 | Electronic Proceedings Article | |
| | 2007 | [Faber, Johannes]
Jacobs, Swen
Sofronie-Stokkermans, Viorica | | Verifying CSP-OZ-DC specifications with complex data types and timing parameters
In: Proceedings of IFM 2007: Integrated Formal Methods, 233-252 | 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 | |
| | 2006 | Jacobs, Swen
Waldmann, Uwe | | Comparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78 | Electronic Journal Article | |
| | 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 | |
| 1 |
| |
| | 1998 | [Jacquemard, Florent]
Meyer, Christoph
Weidenbach, Christoph | | Unification in Extensions of Shallow Equational Theories
In: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), 76-90 | Proceedings Article | |
| 1 |
| |
| | 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 | |
| 1 |
| |
| | 2009 | Horbach, Matthias
Weidenbach, Christoph | | 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 | Proceedings Article | |
| 2 |
| |
| | 2014 | [Kapur, Deepak]
[Zhang, Zhihai]
Horbach, Matthias
[Zhao, Hantao]
[Lu, Qi]
[Nguyen, ThanhVu] | | Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
In: Automated Reasoning and Mathematics: Essays in Memory of William McCune, 189-228 | Part of a Book | |
| | 2013 | [Kapur, Deepak]
[Nieuwenhuis, Robert]
[Voronkov, Andrei]
Weidenbach, Christoph
[Wilhelm, Reinhard] | | Harald Ganzinger's Legacy: Contributions to Logics and Programming
In: Programming Logics, | Proceedings Article | |
| 2 |
| Karl, Carsten |
| |
| | 2007 | Hirth, Simon
Karl, Carsten
Weidenbach, Christoph | | Automatic Analysis of LAN Infrastructures | Report | |
| | 2006 | Karl, Carsten | | Automatische Analyse von Layer 3 Netzwerken mit SPASS
Universität des Saarlandes | Thesis - Masters thesis | |
| 1 |
| |
| | 2013 | [Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas | | Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70 | Proceedings Article | |
| 3 |
| |
| | 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 | |
| | 1998 | Weidenbach, Christoph
Meyer, Christoph
Cohrs, Christian
Engel, Thorsten
Keen, Enno | | SPASS V0.77
In: Journal of Automated Reasoning [21], 113-113 | Journal Article | |
| 1 |
| |
| | 1996 | Weidenbach, Christoph | | Unification in Sort Theories
In: Proceedings of the 10th International Workshop on Unification, UNIF'96, 16-25 | Proceedings Article | |
| 1 |
| |
| | 1996 | [Hähnle, Reiner]
[Kerber, Manfred]
Weidenbach, Christoph | | Common Syntax of the DFG-Schwerpunktprogramm ``Deduktion'' | Report | |
| 1 |
| |
| | 1998 | Weidenbach, Christoph | | Rechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197 | Part of a Book | |
| 1 |
| Kijania-Placek, Katarzyna (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 | |
| 1 |
| |
| | 2008 | [Lynch, Christopher]
Tran, Duc-Khanh | | SMELS: Satisfiability Modulo Equality with Lazy Superposition
In: Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008, 186-200 | Proceedings Article | |
| 2 |
| |
| | 1998 | Nonnengart, Andreas
[Rock, Georg]
Weidenbach, Christoph | | On Generating Small Clause Normal Forms
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 397-411 | Proceedings Article | |
| | 1998 | Waldmann, Uwe | | Superposition for Divisible Torsion-Free Abelian Groups
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 144-159 | Proceedings Article | |
| 1 |
| Kirchner, Helene |
| |
| | 2009 | Tran, Duc-Khanh
[Ringeissen, Christopher]
[Ranise, Silvio]
[Kirchner, Helene] | | Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation
In: Journal of Symbolic Computation [45-], 261-286 | Journal Article | |
| 3 |
| Kirchner, Hélène (ed.) |
| |
| | 1998 | Nonnengart, Andreas
[Rock, Georg]
Weidenbach, Christoph | | On Generating Small Clause Normal Forms
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 397-411 | Proceedings Article | |
| | 1998 | Waldmann, Uwe | | Superposition for Divisible Torsion-Free Abelian Groups
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 144-159 | 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 | |
| 1 |
| Kleine Büning, Hans |
| |
| | 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 | |
| 1 |
| Kolaitis, Phokion (ed.) |
| |
| | 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 | |
| 1 |
| Konev, Boris (ed.) |
| |
| | 2007 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| 2 |
| Korovin, Konstantin |
| |
| | 2006 | Ganzinger, Harald
[Korovin, Konstantin] | | Theory Instantiation
In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06), 497-511 | 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 | |
| 2 |
| |
| | 2013 | [Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas | | Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70 | Proceedings Article | |
| | 2013 | Košta, Marek | | SMT-Based Compiler Support for Memory Access Optimization for Data-Parallel Languages
In: Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences, 36-42 | Proceedings Article | |
| 1 |
| Košta, Marek (ed.) |
| |
| | 2013 | Košta, Marek | | SMT-Based Compiler Support for Memory Access Optimization for Data-Parallel Languages
In: Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences, 36-42 | Proceedings Article | |
| 8 |
| Kruglov, Evgeny |
| |
| | 2013 | Kruglov, Evgeny | | Superposition Modulo Theory
Universität des Saarlandes | Thesis - PhD thesis | |
| | 2012 | Fietzke, Arnaud
Kruglov, Evgeny
Weidenbach, Christoph | | 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 | Proceedings Article | |
| | 2012 | Kruglov, Evgeny
Weidenbach, Christoph | | Superposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456 | Journal Article | |
| | 2012 | Kruglov, Evgeny
Weidenbach, Christoph | | Superposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456 | Journal Article | |
| | 2011 | [Eggers, Andreas]
Kruglov, Evgeny
[Kupferschmid, Stefan]
[Scheibler, Karsten]
[Teige, Teige]
Weidenbach, Christoph | | SUP(NLA) -- Combining Superposition and Non-Linear Arithmetic
In: 8th International Symposium on Frontiers of Combining Systems, 119-134 | Proceedings Article | |
| | 2011 | Kruglov, Evgeny
Weidenbach, Christoph | | SUP(T) Decides First-Order Logic Fragment Over Ground Theories
In: Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS-4), | Proceedings Article | |
| | 2009 | Althaus, Ernst
Kruglov, Evgeny
Weidenbach, Christoph | | Superposition Modulo Linear Arithmetic SUP(LA)
In: Frontiers of Combining Systems : 7th International Symposium, FroCoS 2009, 84-99 | Proceedings Article | |
| | 2008 | Kruglov, Evgeny | | Superposition Modulo Linear Arithmetic
Universität des Saarlandes | Thesis - Masters thesis | |
| 1 |
| |
| | 1994 | Weidenbach, Christoph | | Sorts, Resolution, Tableaux and Propositional Logic
In: KI-94 Workshops: Extended Abstracts, 315-316 | Proceedings Article | |
| 1 |
| |
| | 2011 | [Eggers, Andreas]
Kruglov, Evgeny
[Kupferschmid, Stefan]
[Scheibler, Karsten]
[Teige, Teige]
Weidenbach, Christoph | | SUP(NLA) -- Combining Superposition and Non-Linear Arithmetic
In: 8th International Symposium on Frontiers of Combining Systems, 119-134 | Proceedings Article | |
| 3 |
| |
| | 2009 | Lamotte-Schubert, Manuel
Weidenbach, Christoph | | Analysis of Authorizations in SAP R/3
In: First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving proceedings, 90-104 | Proceedings Article | |
| | 2009 | Lamotte-Schubert, Manuel
Weidenbach, Christoph | | Analysis of Authorizations in SAP R/3
In: FTP 2009 : First-Order Theorem Proving, 90-104 | Electronic Proceedings Article | |
| | 2009 | Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard | | External Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288 | Proceedings Article | |
| 1 |
| |
| | 2008 | Lamotte, Manuel | | Analysis of Authorizations in SAP R/3
Fachhochschule Trier | Thesis - Masters thesis | |
| 1 |
| |
| | 2011 | [Lasaruk, Aless]
Sturm, Thomas | | Automatic Verification of the Adequacy of Models for Families of Geometric Objects
In: Automated Deduction in Geometry : 7th International Workshop, ADG 2008, 116-140 | Proceedings Article | |
| 1 |
| |
| | 2008 | [Lynch, Christopher]
Tran, Duc-Khanh | | SMELS: Satisfiability Modulo Equality with Lazy Superposition
In: Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008, 186-200 | Proceedings Article | |
| 3 |
| |
| | 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 | |
| | 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 |
| Lenzerini, Maurizio (ed.) |
| |
| | 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 | |
| 1 |
| |
| | 2006 | [Lilith, Nimrod]
[Billington, Jonathan]
Freiheit, Jörn | | 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 | Electronic Proceedings Article | |
| 1 |
| |
| | 1998 | [Letz, Reinhold]
Weidenbach, Christoph | | Paradigmen und Perspektiven der automatischen Deduktion
In: KI, Organ des Fachbereichs 1 "Künstliche Intelligenz'' der Gesellschaft für Informatik e.V. [4], 15-19 | Journal Article | |
| 1 |
| |
| | 2010 | Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph | | Model Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21 | Proceedings Article | |
| 1 |
| |
| | 2007 | [Lev-Ami, Tal]
Weidenbach, Christoph
[Reps, Thomas]
[Sagiv, Mooly] | | Labelled Clauses
In: 21st International Conference on Automated Deduction (CADE-21), 311-327 | Proceedings Article | |
| 1 |
| |
| | 1992 | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | | Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434 | Proceedings Article | |
| 1 |
| |
| | 2011 | Sturm, Thomas
[Tiwari, Ashish] | | Verification and Synthesis Using Real Quantifier Elimination
In: ISSAC 2011 : Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation, 329-336 | Proceedings Article | |
| 1 |
| |
| | 2006 | [Lilith, Nimrod]
[Billington, Jonathan]
Freiheit, Jörn | | 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 | Electronic Proceedings Article | |
| 5 |
| |
| | 2003 | [Avenhaus, Jürgen]
Hillenbrand, Thomas
[Löchner, Bernd] | | On Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233 | Journal 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 | |
| | 2002 | [Löchner, Bernd]
Hillenbrand, Thomas | | A Phytography of WALDMEISTER
In: AI Communications [15], 127-133 | Journal Article | |
| | 2002 | Hillenbrand, Thomas
[Löchner, Bernd] | | The Next WALDMEISTER Loop
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 486-500 | Proceedings Article | |
| | 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 | |
| 2 |
| |
| | 2007 | [Ludwig, Michel]
Waldmann, Uwe | | 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 | Proceedings Article | |
| | 2006 | Ludwig, Michel | | Extensions of the Knuth-Bendix Ordering with LPO-like Properties
Universität des Saarlandes | Thesis - Masters thesis | |
| 1 |
| Lutz, Carsten (ed.) |
| |
| | 2008 | Sofronie-Stokkermans, Viorica | | Locality and subsumption testing in $\mathcalEL$ and some of its extensions
In: Proceedings of the 21st International Workshop on Description Logics (DL-2008), 11pages | Electronic Proceedings Article | |
| 1 |
| Luuk, Marc |
| |
| | 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 | |
| 1 |
| Lu, Qi |
| |
| | 2014 | [Kapur, Deepak]
[Zhang, Zhihai]
Horbach, Matthias
[Zhao, Hantao]
[Lu, Qi]
[Nguyen, ThanhVu] | | Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
In: Automated Reasoning and Mathematics: Essays in Memory of William McCune, 189-228 | Part of a Book | |
| 3 |
| Lu, Tianxiang |
| |
| | 2013 | Lu, Tianxiang | | Formal Verification of the Pastry Protocol
Universität des Saarlandes | Thesis - PhD thesis | |
| | 2011 | Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph | | 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 | Proceedings Article | |
| | 2010 | Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph | | Model Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21 | Proceedings Article | |
| 1 |
| Lynch, Christopher |
| |
| | 2008 | [Lynch, Christopher]
Tran, Duc-Khanh | | SMELS: Satisfiability Modulo Equality with Lazy Superposition
In: Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008, 186-200 | Proceedings Article | |
| 1 |
| Lynch, Christopher (ed.) |
| |
| | 2009 | | | UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings | Electronic Proceedings | |
| 1 |
| Maler, Oded (ed.) |
| |
| | 2009 | Jacobs, Swen | | Incremental Instance Generation in Local Reasoning
In: Computer Aided Verification : 21st International Conference, CAV 2009, 368-382 | Proceedings Article | |
| 1 |
| Mantel, Heiko (ed.) |
| |
| | 2006 | Sofronie-Stokkermans, Viorica | | Local reasoning in verification
In: IJCAR'06 Workshop : VERIFY'06: Verification Workshop, 128-145 | Electronic Proceedings Article | |
| 1 |
| Marcus, Solomon (ed.) |
| |
| | 2007 | Sofronie-Stokkermans, Viorica | | Algebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493 | Part of a Book | |
| 2 |
| Matheis, Thomas |
| |
| | 2007 | [Ziemann, Joerg]
[Matheis, Thomas]
Freiheit, Jörn | | Modelling of Cross-Organizational Business Processes
In: Enterprise Modelling and Information Systems Architectures 2007, 87-95 | Proceedings Article | |
| | 2007 | [Ziemann, Joerg]
[Matheis, Thomas]
Freiheit, Jörn | | Modelling of Cross-Organizational Business Processes - Current Methods and Standards
In: Enterprise Modelling and Information Systems Architectures [2], 23-31 | Journal Article | |
| 2 |
| |
| | 2000 | Sofronie-Stokkermans, Viorica | | On unification for bounded distributive lattices
In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), 465-481 | Proceedings Article | |
| | 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 | |
| 1 |
| McCune, William (ed.) |
| |
| | 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 | |
| 1 |
| McRobbie, Michael A. (ed.) |
| |
| | 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 | |
| 2 |
| McRobbie, M. A. (ed.) |
| |
| | 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 | |
| | 1996 | Weidenbach, Christoph | | Unification in Pseudo-Linear Sort Theories is Decidable
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 343-357 | Proceedings Article | |
| 1 |
| |
| | 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 | |
| 1 |
| |
| | 2009 | Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard | | External Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288 | Proceedings Article | |
| 1 |
| |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies
In: Integrated Formal Methods : 8th International Conference, IFM 2010, 152-167 | Proceedings Article | |
| 3 |
| |
| | 2012 | [Fontaine, Pascal]
[Merz, Stephan]
Weidenbach, Christoph | | Combination of Disjoint Theories: Beyond Decidability
In: Proceedings of the 6th International Joint Conference on Automated Reasoning, | Proceedings Article | |
| | 2011 | Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph | | 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 | Proceedings Article | |
| | 2010 | Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph | | Model Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21 | Proceedings Article | |
| 1 |
| |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies
In: Integrated Formal Methods : 8th International Conference, IFM 2010, 152-167 | Proceedings Article | |
| 3 |
| |
| | 1998 | Weidenbach, Christoph
Meyer, Christoph
Cohrs, Christian
Engel, Thorsten
Keen, Enno | | SPASS V0.77
In: Journal of Automated Reasoning [21], 113-113 | Journal Article | |
| | 1998 | [Jacquemard, Florent]
Meyer, Christoph
Weidenbach, Christoph | | Unification in Extensions of Shallow Equational Theories
In: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), 76-90 | 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 | |
| 1 |
| |
| | 2012 | Suda, Martin
Weidenbach, Christoph | | A PLTL-prover based on labelled superposition with partial model guidance
In: Automated Reasoning : 6th International Joint Conference, IJCAR 2012, 537-543 | Proceedings Article | |
| 1 |
| |
| | 2008 | Sofronie-Stokkermans, Viorica | | Locality and subsumption testing in $\mathcalEL$ and some of its extensions
In: Proceedings of the 21st International Workshop on Description Logics (DL-2008), 11pages | Electronic Proceedings Article | |
| 1 |
| |
| | 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 | |
| 1 |
| |
| | 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 |
| |
| | 2003 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| 1 |
| |
| | 2007 | [Damm, Werner]
[Disch, Stefan]
[Hungar, Hardi]
Jacobs, Swen
[Pang, Jun]
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | 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 | Proceedings Article | |
| 1 |
| |
| | 2003 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| 1 |
| |
| | 2009 | | | UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings | Electronic Proceedings | |
| 1 |
| |
| | 2009 | Neumann, Stephan Rouven | | Automated Proof Generation of Possibiltiy Properties in Inductive Protocol Verification
Universität des Saarlandes | Thesis - Bachelor thesis | |
| 1 |
| |
| | 2014 | [Kapur, Deepak]
[Zhang, Zhihai]
Horbach, Matthias
[Zhao, Hantao]
[Lu, Qi]
[Nguyen, ThanhVu] | | Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
In: Automated Reasoning and Mathematics: Essays in Memory of William McCune, 189-228 | Part of a Book | |
| 2 |
| |
| | 2013 | [Kapur, Deepak]
[Nieuwenhuis, Robert]
[Voronkov, Andrei]
Weidenbach, Christoph
[Wilhelm, Reinhard] | | Harald Ganzinger's Legacy: Contributions to Logics and Programming
In: Programming Logics, | 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 | |
| 3 |
| Nieuwenhuis, Robert (ed.) |
| |
| | 2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Jacobs, Swen | | Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
In: Deduction and Decision Procedures, 1-22 | Electronic Proceedings Article | |
| | 2005 | Sofronie-Stokkermans, Viorica | | Hierarchic reasoning in local theory extensions
In: Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 219-234 | Proceedings Article | |
| | 2001 | Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph | | First-Order Atom Definitions Extended
In: Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001), 309-319 | Proceedings Article | |
| 4 |
| Nipkow, Tobias (ed.) |
| |
| | 2010 | Sofronie-Stokkermans, Viorica | | 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 | Electronic 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 | |
| | 1998 | [Jacquemard, Florent]
Meyer, Christoph
Weidenbach, Christoph | | Unification in Extensions of Shallow Equational Theories
In: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), 76-90 | Proceedings Article | |
| 3 |
| |
| | 2001 | Nonnengart, Andreas
Weidenbach, Christoph | | Computing small clause normal forms
In: Handbook of Automated Reasoning, 335-367 | Part of a Book | |
| | 1998 | Nonnengart, Andreas
[Rock, Georg]
Weidenbach, Christoph | | On Generating Small Clause Normal Forms
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 397-411 | 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 | |
| 1 |
| |
| | 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 | |
| 1 |
| |
| | 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 | |
| 2 |
| |
| | 1995 | Ohlbach, Hans Jürgen
Weidenbach, Christoph | | A Note on Assumptions about Skolem Functions
In: Journal of Automated Reasoning [15], 267-275 | Journal 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 | |
| 1 |
| Ohlbach, Hans Jürgen (ed.) |
| |
| | 1993 | Weidenbach, Christoph | | A New Sorted Logic
In: GWAI-92: Advances in Artificial Inteligence, Proceedings 16th German Workshop on Artificial Intelligence, 43-54 | Proceedings Article | |
| 1 |
| Okamura, Yoshio (ed.) |
| |
| | 2007 | [Damm, Werner]
[Disch, Stefan]
[Hungar, Hardi]
Jacobs, Swen
[Pang, Jun]
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | 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 | Proceedings Article | |
| 1 |
| Olbrich, Sebastian |
| |
| | 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 | |
| 8 |
| Olderog, Ernst-Rüdiger (ed.) |
| |
| | 2011 | [Damm, Werner]
[Disch, Stefan]
Hagemann, Willem
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Integrating incremental flow pipes into a symbolic model checker for hybrid systems | Report | |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | PTIME parametric verification of safety properties for reasonable linear hybrid automata | Report | |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies | Report | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | On hierarchical reasoning in combinations of theories | Report | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | System Description: H-PILoT (Version 1.9) | Report | |
| | 2009 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation | Report | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Efficient Hierarchical Reasoning about Functions over Numerical Domains | Report | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Sheaves and geometric logic and applications to modular verification of complex systems | Report | |
| 3 |
| |
| | 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 | |
| | 2000 | [Iturrioz, Luisa]
Sofronie-Stokkermans, Viorica | | SHn-algebras (Symmetric Heyting algebras of order n)
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-11 | Part of a Book | |
| | 2000 | Sofronie-Stokkermans, Viorica | | Some properties of Kleene algebras
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-7 | Part of a Book | |
| 2 |
| |
| | 2007 | [Damm, Werner]
[Disch, Stefan]
[Hungar, Hardi]
Jacobs, Swen
[Pang, Jun]
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | 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 | Proceedings Article | |
| | 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 | |
| 1 |
| Pascal Fontaine (ed.) |
| |
| | 2013 | [Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas | | Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70 | Proceedings Article | |
| 1 |
| Patel-Schneider, Peter F. (ed.) |
| |
| | 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 | |
| 1 |
| Paun, Gheorghe (ed.) |
| |
| | 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 | |
| 1 |
| Peltier, Nicolas |
| |
| | 2012 | [Peltier, Nicolas]
Sofronie-Stokkermans, Viorica | | First-order theorem proving: Foreword
In: Journal of Symbolic Computation [47], 1009-1010 | Journal Article | |
| 5 |
| Peltier, Nicolas (ed.) |
| |
| | 2010 | | | First-Order Theorem Proving : Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09) | Electronic Proceedings | |
| | 2009 | Lamotte-Schubert, Manuel
Weidenbach, Christoph | | Analysis of Authorizations in SAP R/3
In: First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving proceedings, 90-104 | Proceedings Article | |
| | 2009 | Lamotte-Schubert, Manuel
Weidenbach, Christoph | | Analysis of Authorizations in SAP R/3
In: FTP 2009 : First-Order Theorem Proving, 90-104 | Electronic Proceedings Article | |
| | 2009 | | | First-Order Theorem Proving 2009 | Proceedings | |
| | 2009 | | | First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving, Proceedings | Proceedings | |
| 1 |
| Pfenning, Frank (ed.) |
| |
| | 2007 | Weidenbach, Christoph
[Schmidt, Renate]
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor | | System Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520 | Proceedings Article | |
| 4 |
| Pigorsch, Florian |
| |
| | 2012 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
In: Science of Computer Programming [77], 1122-1150 | Journal Article | |
| | 2011 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces
In: Science of Computer Programming [in press], 1-29 | Electronic Journal Article | |
| | 2007 | [Damm, Werner]
[Disch, Stefan]
[Hungar, Hardi]
Jacobs, Swen
[Pang, Jun]
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | 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 | Proceedings Article | |
| | 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 | |
| 1 |
| |
| | 2013 | Hillenbrand, Thomas
[Piskac, Ruzica]
Waldmann, Uwe
Weidenbach, Christoph | | From Search to Computation: Redundancy Criteria and Simplification at Work
In: Programming Logics, Essays in Memory of Harald Ganzinger, ? | Part of a Book | |
| 1 |
| |
| | 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 | |
| 9 |
| |
| | 2011 | [Damm, Werner]
[Disch, Stefan]
Hagemann, Willem
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Integrating incremental flow pipes into a symbolic model checker for hybrid systems | Report | |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | PTIME parametric verification of safety properties for reasonable linear hybrid automata | Report | |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies | Report | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | On hierarchical reasoning in combinations of theories | Report | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | System Description: H-PILoT (Version 1.9) | Report | |
| | 2009 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation | Report | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Efficient Hierarchical Reasoning about Functions over Numerical Domains | Report | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Sheaves and geometric logic and applications to modular verification of complex systems | Report | |
| | 2007 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation
In: Verification, Model Checking and Abstract Interpretation : 8th International Conference, VMCAI 2007, 346-362 | Proceedings Article | |
| 1 |
| |
| | 2012 | [Blanchette, Jasmin Christian]
[Popescu, Andrei]
Wand, Daniel
Weidenbach, Christoph | | More SPASS with Isabelle : Superposition with Hard Sorts and Configurable Simplification
In: Interactive Theorem Proving : Third International Conference, ITP 2012, 345-360 | Proceedings Article | |
| 1 |
| |
| | 1998 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| 1 |
| |
| | 2006 | [Prevosto, Virgile]
Waldmann, Uwe | | SPASS+T
In: ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 18-33 | Proceedings Article | |
| 1 |
| |
| | 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 | |
| 1 |
| Ramakrishnan, C. R. (ed.) |
| |
| | 2008 | Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica | | On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281 | Proceedings Article | |
| 1 |
| |
| | 2009 | Tran, Duc-Khanh
[Ringeissen, Christopher]
[Ranise, Silvio]
[Kirchner, Helene] | | Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation
In: Journal of Symbolic Computation [45-], 261-286 | Journal Article | |
| 1 |
| |
| | 2007 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| 2 |
| |
| | 2011 | Fietzke, Arnaud
Weidenbach, Christoph | | Superposition as a Decision Procedure for Timed Automata
In: Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2011), | Proceedings Article | |
| | 2011 | Kruglov, Evgeny
Weidenbach, Christoph | | SUP(T) Decides First-Order Logic Fragment Over Ground Theories
In: Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS-4), | Proceedings Article | |
| 1 |
| Rehof, Jakob (ed.) |
| |
| | 2008 | Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica | | On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281 | Proceedings Article | |
| 1 |
| Reischuk, Rüdiger (ed.) |
| |
| | 1998 | Weidenbach, Christoph | | Rechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197 | Part of a Book | |
| 1 |
| Remenyi, Dan (ed.) |
| |
| | 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 | |
| 1 |
| Rémy, J.-L. (ed.) |
| |
| | 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 | |
| 1 |
| Renate A. Schmidt (ed.) |
| |
| | 2013 | [Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas | | Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70 | Proceedings Article | |
| 1 |
| Reps, Thomas |
| |
| | 2007 | [Lev-Ami, Tal]
Weidenbach, Christoph
[Reps, Thomas]
[Sagiv, Mooly] | | Labelled Clauses
In: 21st International Conference on Automated Deduction (CADE-21), 311-327 | Proceedings Article | |
| 1 |
| Reuter, Jochen |
| |
| | 2013 | Reuter, Jochen | | Real Linear Quantifier Elimination
Universität des Saarlandes | Thesis - Masters thesis | |
| 1 |
| Riazanov, Alexandre |
| |
| | 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 | |
| 1 |
| Ringeissen, Christophe (ed.) |
| |
| | 2013 | Horbach, Matthias
Sofronie-Stokkermans, Viorica | | Obtaining Finite Local Theory Axiomatizations via Saturation
In: Frontiers of Combining Systems - 9th International Symposium, 198-213 | Proceedings Article | |
| 1 |
| Ringeissen, Christopher |
| |
| | 2009 | Tran, Duc-Khanh
[Ringeissen, Christopher]
[Ranise, Silvio]
[Kirchner, Helene] | | Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation
In: Journal of Symbolic Computation [45-], 261-286 | Journal Article | |
| 2 |
| Robinson, Alan (ed.) |
| |
| | 2001 | Weidenbach, Christoph | | Combining Superposition, Sorts and Splitting
In: Handbook of Automated Reasoning, 1965-2013 | Part of a Book | |
| | 2001 | Nonnengart, Andreas
Weidenbach, Christoph | | Computing small clause normal forms
In: Handbook of Automated Reasoning, 335-367 | Part of a Book | |
| 2 |
| |
| | 1998 | Nonnengart, Andreas
[Rock, Georg]
Weidenbach, Christoph | | On Generating Small Clause Normal Forms
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 397-411 | Proceedings Article | |
| | 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 | |
| 1 |
| Roggenbach, Markus (ed.) |
| |
| | 2010 | Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph | | Model Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21 | Proceedings Article | |
| 1 |
| Rosati, Riccardo (ed.) |
| |
| | 2011 | Gasse, Francis
Sofronie-Stokkermans, Viorica | | 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 | Electronic Proceedings Article | |
| 1 |
| Rudeanu, Sergiu (ed.) |
| |
| | 2007 | Sofronie-Stokkermans, Viorica | | Algebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493 | Part of a Book | |
| 1 |
| Rudolph, Sebastian (ed.) |
| |
| | 2011 | Gasse, Francis
Sofronie-Stokkermans, Viorica | | 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 | Electronic Proceedings Article | |
| 1 |
| Rump, Frank J. (ed.) |
| |
| | 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 | |
| 2 |
| Rusev, Rostislav |
| |
| | 2008 | Rusev, Rostislav | | Bitvector Reasoning with SPASS
Universität des Saarlandes | Thesis - Masters thesis | |
| | 2007 | Weidenbach, Christoph
[Schmidt, Renate]
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor | | System Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520 | Proceedings Article | |
| 1 |
| Rusinowitch, Michael (ed.) |
| |
| | 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 | |
| 1 |
| |
| | 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 | |
| 3 |
| |
| | 2010 | [Rybalchenko, Andrey]
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation
In: Journal of Symbolic Computation [45], 1212-1233 | Journal Article | |
| | 2009 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation | Report | |
| | 2007 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation
In: Verification, Model Checking and Abstract Interpretation : 8th International Conference, VMCAI 2007, 346-362 | Proceedings Article | |
| 1 |
| |
| | 2007 | [Lev-Ami, Tal]
Weidenbach, Christoph
[Reps, Thomas]
[Sagiv, Mooly] | | Labelled Clauses
In: 21st International Conference on Automated Deduction (CADE-21), 311-327 | Proceedings Article | |
| 1 |
| |
| | 1996 | Weidenbach, Christoph | | Sorted Unification and Its Application to Automated Theorem Proving
In: Proceedings of the CADE-13 Workshop: Term Schematizations and Their Applications, 67-76 | Proceedings Article | |
| 1 |
| |
| | 2003 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| 1 |
| |
| | 2012 | Suda, Martin
Weidenbach, Christoph | | A PLTL-prover based on labelled superposition with partial model guidance
In: Automated Reasoning : 6th International Joint Conference, IJCAR 2012, 537-543 | Proceedings Article | |
| 1 |
| |
| | 2010 | [Ghilardi, Silvio]
[Sattler, Ulrike]
Sofronie-Stokkermans, Viorica
[Tiwari, Ashish] | | Special issue on automated deduction: Decidability, complexity, tractability
In: Journal of Symbolic Computation [45], 151-152 | Journal Article | |
| 4 |
| |
| | 2008 | | | Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08) | Proceedings | |
| | 2008 | Jacobs, Swen | | Incremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62 | Proceedings Article | |
| | 2007 | | | Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07) | Proceedings | |
| | 2004 | Hillenbrand, Thomas | | A Superposition View on Nelson-Oppen
In: Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning, 16-20 | Electronic Proceedings Article | |
| 1 |
| Scheibler, Karsten |
| |
| | 2011 | [Eggers, Andreas]
Kruglov, Evgeny
[Kupferschmid, Stefan]
[Scheibler, Karsten]
[Teige, Teige]
Weidenbach, Christoph | | SUP(NLA) -- Combining Superposition and Non-Linear Arithmetic
In: 8th International Symposium on Frontiers of Combining Systems, 119-134 | Proceedings Article | |
| 1 |
| Schmidt, Renate |
| |
| | 2007 | Weidenbach, Christoph
[Schmidt, Renate]
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor | | System Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520 | Proceedings Article | |
| 2 |
| Schmidt, Renate A. |
| |
| | 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 | |
| | 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 | |
| 6 |
| |
| | 2013 | Horbach, Matthias
Sofronie-Stokkermans, Viorica | | Obtaining Finite Local Theory Axiomatizations via Saturation
In: Frontiers of Combining Systems - 9th International Symposium, 198-213 | Proceedings Article | |
| | 2009 | Horbach, Matthias
Weidenbach, Christoph | | Decidability Results for Saturation-Based Model Building
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 404-420 | Proceedings Article | |
| | 2009 | Sofronie-Stokkermans, Viorica | | Locality results for certain extensions of theories with bridging functions
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 67-83 | Proceedings Article | |
| | 2009 | Weidenbach, Christoph
Dimova, Dilyana
Fietzke, Arnaud
Suda, Martin
Wischnewski, Patrick | | SPASS Version 3.5
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 140-145 | Proceedings Article | |
| | 2009 | [Baumgartner, Peter]
Waldmann, Uwe | | Superposition and Model Evolution Combined
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 17-34 | Proceedings Article | |
| | 2009 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | System Description: H-PILoT
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 131-139 | Proceedings Article | |
| 1 |
| Schmidt, Renate (ed.) |
| |
| | 2006 | [Prevosto, Virgile]
Waldmann, Uwe | | SPASS+T
In: ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 18-33 | Proceedings Article | |
| 1 |
| Schmitt, Peter H. (ed.) |
| |
| | 1998 | Weidenbach, Christoph | | Sorted Unification and Tree Automata
In: Automated Deduction - A Basis for Applications, 291-320 | Part of a Book | |
| 5 |
| Scholl, Christoph |
| |
| | 2012 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
In: Science of Computer Programming [77], 1122-1150 | Journal Article | |
| | 2011 | [Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces
In: Science of Computer Programming [in press], 1-29 | Electronic Journal Article | |
| | 2011 | [Damm, Werner]
[Disch, Stefan]
Hagemann, Willem
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | Integrating incremental flow pipes into a symbolic model checker for hybrid systems | Report | |
| | 2007 | [Damm, Werner]
[Disch, Stefan]
[Hungar, Hardi]
Jacobs, Swen
[Pang, Jun]
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris] | | 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 | Proceedings Article | |
| | 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 | |
| 1 |
| Schulz, Klaus U. (ed.) |
| |
| | 1996 | Weidenbach, Christoph | | Unification in Sort Theories
In: Proceedings of the 10th International Workshop on Unification, UNIF'96, 16-25 | Proceedings Article | |
| 2 |
| Schulz, Stephan (ed.) |
| |
| | 2006 | [Prevosto, Virgile]
Waldmann, Uwe | | SPASS+T
In: ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 18-33 | Proceedings Article | |
| | 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 | |
| 2 |
| Sebastiani, Roberto (ed.) |
| |
| | 2009 | Althaus, Ernst
Kruglov, Evgeny
Weidenbach, Christoph | | Superposition Modulo Linear Arithmetic SUP(LA)
In: Frontiers of Combining Systems : 7th International Symposium, FroCoS 2009, 84-99 | 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 |
| Seiler, W. |
| |
| | 2013 | [Errami, H.]
[Eiswirth, M.]
[Grigoriev. D.]
[Seiler, W.]
Sturm, T.
[Weber, A.] | | Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates
In: Proceedings of the CASC 2013, 88-99 | Proceedings Article | |
| 1 |
| Shankar, Natarajan (ed.) |
| |
| | 2006 | Sofronie-Stokkermans, Viorica | | Interpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250 | Proceedings Article | |
| 1 |
| Sigayret, Alain (ed.) |
| |
| | 2003 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| 1 |
| Sijanski, Grozdana |
| |
| | 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 | |
| 1 |
| Simon, Carlo |
| |
| | 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 | |
| 1 |
| Slaney, John K. (ed.) |
| |
| | 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 | |
| 2 |
| Slaney, J. K. (ed.) |
| |
| | 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 | |
| | 1996 | Weidenbach, Christoph | | Unification in Pseudo-Linear Sort Theories is Decidable
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 343-357 | Proceedings Article | |
| 75 |
| Sofronie-Stokkermans, Viorica |
| |
| | 2013 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| | 2013 | Sofronie-Stokkermans, Viorica | | Locality and Applications to Subsumption Testing in EL and Some of its Extensions
In: Scientific Annals of Computer Science [23], 251-284 | Journal Article | |
| | 2013 | Horbach, Matthias
Sofronie-Stokkermans, Viorica | | Obtaining Finite Local Theory Axiomatizations via Saturation
In: Frontiers of Combining Systems - 9th International Symposium, 198-213 | Proceedings Article | |
| | 2013 | Sofronie-Stokkermans, Viorica | | On combinations of local theory extensions
In: Programming Logics, Essays in Memory of Harald Ganzinger, 392-413 | Part of a Book | |
| | 2013 | [Bjorner, Nikolaj]
Sofronie-Stokkermans, Viorica | | Preface: Special Issue of Selected Extended Papers of CADE-23
In: Journal of Automated Reasoning [51], 1-2 | Journal Article | |
| | 2012 | [Peltier, Nicolas]
Sofronie-Stokkermans, Viorica | | First-order theorem proving: Foreword
In: Journal of Symbolic Computation [47], 1009-1010 | Journal Article | |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| | 2011 | Gasse, Francis
Sofronie-Stokkermans, Viorica | | 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 | Electronic Proceedings Article | |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | PTIME parametric verification of safety properties for reasonable linear hybrid automata | Report | |
| | 2011 | [Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | PTIME parametric verification of safety properties for reasonable linear hybrid automata
In: Mathematics in Computer Science [5], 469-497 | Journal Article | |
| | 2010 | Sofronie-Stokkermans, Viorica | | 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 | Electronic Proceedings Article | |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies | Report | |
| | 2010 | [Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica | | Automatic Verification of Parametric Specifications with Complex Topologies
In: Integrated Formal Methods : 8th International Conference, IFM 2010, 152-167 | Proceedings Article | |
| | 2010 | [Rybalchenko, Andrey]
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation
In: Journal of Symbolic Computation [45], 1212-1233 | Journal Article | |
| | 2010 | Sofronie-Stokkermans, Viorica | | Hierarchical Reasoning for the Verification of Parametric Systems
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 171-187 | Proceedings Article | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | On hierarchical reasoning in combinations of theories | Report | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | On Hierarchical Reasoning in Combinations of Theories
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 30-45 | Proceedings Article | |
| | 2010 | [Ghilardi, Silvio]
[Sattler, Ulrike]
Sofronie-Stokkermans, Viorica
[Tiwari, Ashish] | | Special issue on automated deduction: Decidability, complexity, tractability
In: Journal of Symbolic Computation [45], 151-152 | Journal Article | |
| | 2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | System Description: H-PILoT (Version 1.9) | Report | |
| | 2009 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation | Report | |
| | 2009 | Sofronie-Stokkermans, Viorica | | Locality results for certain extensions of theories with bridging functions
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 67-83 | Proceedings Article | |
| | 2009 | Sofronie-Stokkermans, Viorica | | Reasoning in Complex Theories and Applications. Advanced Lecture
In: ESSLLI 2009 : European Summer School in Logic, Language and Information, 1-64 | Electronic Proceedings Article | |
| | 2009 | Sofronie-Stokkermans, Viorica | | Sheaves and geometric logic and applications to modular verification of complex systems
In: Electronic Notes in Theoretical Computer Science [230], 161-187 | Electronic Journal Article | |
| | 2009 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | | System Description: H-PILoT
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 131-139 | Proceedings Article | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Efficient Hierarchical Reasoning about Functions over Numerical Domains | Report | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Efficient hierarchical reasoning about functions over numerical domains
In: KI 2008: Advances in Artificial Intelligence, 135-143 | Proceedings Article | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Interpolation in local theory extensions
In: Logical Methods in Computer Science [4], 31 pages | Electronic Journal Article | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Locality and subsumption testing in $\mathcalEL$ and some of its extensions
In: Advances in Modal Logic, Vol.7 (Proceedings of AIML 2008), 315-339 | Proceedings Article | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Locality and subsumption testing in $\mathcalEL$ and some of its extensions
In: Proceedings of the 21st International Workshop on Description Logics (DL-2008), 11pages | Electronic Proceedings Article | |
| | 2008 | Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica | | On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281 | Proceedings Article | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Reasoning in Complex Theories and Applications | Miscellaneous | |
| | 2008 | Sofronie-Stokkermans, Viorica | | Sheaves and geometric logic and applications to modular verification of complex systems | Report | |
| | 2007 | Sofronie-Stokkermans, Viorica | | Algebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493 | Part of a Book | |
| | 2007 | Jacobs, Swen
Sofronie-Stokkermans, Viorica | | Applications of hierarchical reasoning in the verification of complex systems
In: Electronic Notes in Theoretical Computer Science [174], 39-54 | Electronic Journal Article | |
| | 2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten | | Automated reasoning in some local extensions of ordered structures
In: Journal of Multiple-Valued Logic and Soft Computing [13], 397-414 | Journal Article | |
| | 2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten | | Automated reasoning in some local extensions of ordered structures
In: Proceedings of ISMVL 2007, Article1 | Proceedings Article | |
| | 2007 | Sofronie-Stokkermans, Viorica | | Automated theorem proving by resolution in non-classical logics
In: Annals of Mathematics and Artificial Intelligence [49], 221-252 | Journal Article | |
| | 2007 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | | Constraint Solving for Interpolation
In: Verification, Model Checking and Abstract Interpretation : 8th International Conference, VMCAI 2007, 346-362 | Proceedings Article | |
| | 2007 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| | 2007 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| | 2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Jacobs, Swen | | Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
In: Deduction and Decision Procedures, 1-22 | Electronic Proceedings Article | |
| | 2007 | Sofronie-Stokkermans, Viorica | | On unification for bounded distributive lattices
In: ACM Transactions on Computational Logic [8], 12.1-12.28 | Journal Article | |
| | 2007 | Sofronie-Stokkermans, Viorica | | On unification in certain finitely generated varieties of algebras
In: Proceedings of the 21th International Workshop on Unification (UNIF 2007), 1-5 | Electronic Proceedings Article | |
| | 2007 | [Faber, Johannes]
Jacobs, Swen
Sofronie-Stokkermans, Viorica | | Verifying CSP-OZ-DC specifications with complex data types and timing parameters
In: Proceedings of IFM 2007: Integrated Formal Methods, 233-252 | 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 | |
| | 2006 | Sofronie-Stokkermans, Viorica | | Automatisches Beweisen in komplexen Theorien
In: MPG Jahrbuch [-], | Electronic Journal Article | |
| | 2006 | Sofronie-Stokkermans, Viorica | | Interpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250 | Proceedings Article | |
| | 2006 | Sofronie-Stokkermans, Viorica | | Local reasoning in verification
In: IJCAR'06 Workshop : VERIFY'06: Verification Workshop, 128-145 | Electronic Proceedings Article | |
| | 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 | Sofronie-Stokkermans, Viorica | | Sheaves and geometric logic in concurrency
In: Proceedings of the Eighth Workshop on Geometric and Topological Methods in Concurrency (GETCO 2006), ? | Proceedings Article | |
| | 2005 | Sofronie-Stokkermans, Viorica | | Hierarchic reasoning in local theory extensions
In: Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 219-234 | Proceedings Article | |
| | 2004 | Sofronie-Stokkermans, Viorica | | Algebraic and logical methods in automated theorem proving and in the study of concurrency
Universität des Saarlandes | Thesis - Habilitation thesis | |
| | 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 | |
| | 2004 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| | 2003 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| | 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 | |
| | 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 | |
| | 2001 | Sofronie-Stokkermans, Viorica | | 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 | Journal Article | |
| | 2001 | Sofronie-Stokkermans, Viorica | | Representation theorems and the semantics of (semi)lattice-based logics
In: Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logics, 125-134 | Proceedings Article | |
| | 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 | Sofronie-Stokkermans, Viorica | | 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 | Journal Article | |
| | 2000 | Sofronie-Stokkermans, Viorica | | 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 | Journal Article | |
| | 2000 | Sofronie-Stokkermans, Viorica | | On unification for bounded distributive lattices
In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), 465-481 | Proceedings Article | |
| | 2000 | Sofronie-Stokkermans, Viorica | | 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 | Journal Article | |
| | 2000 | Sofronie-Stokkermans, Viorica | | Resolution-based theorem proving for SHn-logics
In: Automated Deduction in Classical and Non-Classical Logic (Selected Papers of FTP'98), 268-282 | Proceedings Article | |
| | 2000 | [Iturrioz, Luisa]
Sofronie-Stokkermans, Viorica | | SHn-algebras (Symmetric Heyting algebras of order n)
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-11 | Part of a Book | |
| | 2000 | Sofronie-Stokkermans, Viorica | | Some properties of Kleene algebras
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-7 | Part of a Book | |
| | 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 | |
| | 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 | 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 | |
| | 1999 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| | 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 | |
| | 1998 | Sofronie-Stokkermans, Viorica | | 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 | Proceedings Article | |
| | 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 | |
| | 1998 | Sofronie-Stokkermans, Viorica | | Resolution-based Theorem Proving for SHn-Logics | Report | |
| 12 |
| Sofronie-Stokkermans, Viorica (ed.) |
| |
| | 2011 | | | Automated Deduction - CADE-23 : 23rd International Conference on Automated Deduction | Proceedings | |
| | 2011 | | | Frontiers of Combining Systems | Proceedings | |
| | 2011 | [Eggers, Andreas]
Kruglov, Evgeny
[Kupferschmid, Stefan]
[Scheibler, Karsten]
[Teige, Teige]
Weidenbach, Christoph | | SUP(NLA) -- Combining Superposition and Non-Linear Arithmetic
In: 8th International Symposium on Frontiers of Combining Systems, 119-134 | Proceedings Article | |
| | 2010 | | | First-Order Theorem Proving : Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09) | Electronic Proceedings | |
| | 2009 | Lamotte-Schubert, Manuel
Weidenbach, Christoph | | Analysis of Authorizations in SAP R/3
In: First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving proceedings, 90-104 | Proceedings Article | |
| | 2009 | Lamotte-Schubert, Manuel
Weidenbach, Christoph | | Analysis of Authorizations in SAP R/3
In: FTP 2009 : First-Order Theorem Proving, 90-104 | Electronic Proceedings Article | |
| | 2009 | | | First-Order Theorem Proving 2009 | Proceedings | |
| | 2009 | | | First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving, Proceedings | Proceedings | |
| | 2009 | | | UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings | Electronic Proceedings | |
| | 2008 | | | Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08) | Proceedings | |
| | 2008 | Jacobs, Swen | | Incremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62 | Proceedings Article | |
| | 2007 | | | Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07) | Proceedings | |
| 1 |
| Spies, Hendrik |
| |
| | 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 |
| Stickel, Mark E. (ed.) |
| |
| | 2014 | [Kapur, Deepak]
[Zhang, Zhihai]
Horbach, Matthias
[Zhao, Hantao]
[Lu, Qi]
[Nguyen, ThanhVu] | | Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
In: Automated Reasoning and Mathematics: Essays in Memory of William McCune, 189-228 | Part of a Book | |
| 1 |
| Stickel, Mark (ed.) |
| |
| | 2013 | Hillenbrand, Thomas
Weidenbach, Christoph | | Superposition for Bounded Domains
In: Automated Reasoning and Mathematics, Essays in Memory of William W. McCune, 68-100 | Part of a Book | |
| 1 |
| Stokkermans, Karel |
| |
| | 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 | |
| 1 |
| Stoyan, Herbert (ed.) |
| |
| | 1994 | Weidenbach, Christoph | | Sorts, Resolution, Tableaux and Propositional Logic
In: KI-94 Workshops: Extended Abstracts, 315-316 | Proceedings Article | |
| 4 |
| Sturm, Thomas |
| |
| | 2013 | [Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas | | Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70 | Proceedings Article | |
| | 2011 | [Weber, Andreas]
Sturm, Thomas
[Abdel-Rahman, Essam O.] | | Algorithmic Global Criteria for Excluding Oscillations
In: Bulletin of Mathematical Biology [73], 899-916 | Journal Article | |
| | 2011 | [Lasaruk, Aless]
Sturm, Thomas | | Automatic Verification of the Adequacy of Models for Families of Geometric Objects
In: Automated Deduction in Geometry : 7th International Workshop, ADG 2008, 116-140 | Proceedings Article | |
| | 2011 | Sturm, Thomas
[Tiwari, Ashish] | | Verification and Synthesis Using Real Quantifier Elimination
In: ISSAC 2011 : Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation, 329-336 | Proceedings Article | |
| 3 |
| |
| | 2013 | Košta, Marek | | SMT-Based Compiler Support for Memory Access Optimization for Data-Parallel Languages
In: Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences, 36-42 | Proceedings Article | |
| | 2011 | | | Automated Deduction in Geometry : 7th International Workshop, ADG 2008 | Proceedings | |
| | 2011 | [Lasaruk, Aless]
Sturm, Thomas | | Automatic Verification of the Adequacy of Models for Families of Geometric Objects
In: Automated Deduction in Geometry : 7th International Workshop, ADG 2008, 116-140 | Proceedings Article | |
| 1 |
| |
| | 2013 | [Errami, H.]
[Eiswirth, M.]
[Grigoriev. D.]
[Seiler, W.]
Sturm, T.
[Weber, A.] | | Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates
In: Proceedings of the CASC 2013, 88-99 | Proceedings Article | |
| 6 |
| |
| | 2012 | Suda, Martin
Weidenbach, Christoph | | A PLTL-prover based on labelled superposition with partial model guidance
In: Automated Reasoning : 6th International Joint Conference, IJCAR 2012, 537-543 | Proceedings Article | |
| | 2012 | Suda, Martin
Weidenbach, Christoph | | Labelled Superposition for PLTL
In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, 391-405 | Proceedings Article | |
| | 2010 | Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick | | On the Saturation of YAGO | Report | |
| | 2010 | Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick | | On the Saturation of YAGO
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 441-456 | Proceedings Article | |
| | 2009 | Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard | | External Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288 | Proceedings Article | |
| | 2009 | Weidenbach, Christoph
Dimova, Dilyana
Fietzke, Arnaud
Suda, Martin
Wischnewski, Patrick | | SPASS Version 3.5
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 140-145 | Proceedings Article | |
| 1 |
| Sutcliffe, Geoff |
| |
| | 2009 | Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard | | External Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288 | Proceedings Article | |
| 1 |
| Sutcliffe, Geoff (ed.) |
| |
| | 2006 | [Prevosto, Virgile]
Waldmann, Uwe | | SPASS+T
In: ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 18-33 | Proceedings Article | |
| 1 |
| Tang, Ching Hoo |
| |
| | 2013 | [Dhungana, Deepak]
Tang, Ching Hoo
Weidenbach, Christoph
[Wischnewski, Patrick] | | Automated Verification of Interactive Rule-Based Configuration Systems
In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 551-561 | Proceedings Article | |
| 1 |
| Teige, Teige |
| |
| | 2011 | [Eggers, Andreas]
Kruglov, Evgeny
[Kupferschmid, Stefan]
[Scheibler, Karsten]
[Teige, Teige]
Weidenbach, Christoph | | SUP(NLA) -- Combining Superposition and Non-Linear Arithmetic
In: 8th International Symposium on Frontiers of Combining Systems, 119-134 | Proceedings Article | |
| 1 |
| Teucke, Andreas |
| |
| | 2013 | Teucke, Andreas | | CDCL with Reduction
Universität des Saarlandes | Thesis - Masters thesis | |
| 2 |
| Theobalt, Christian |
| |
| | 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 | |
| 2 |
| |
| | 2011 | | | Frontiers of Combining Systems | Proceedings | |
| | 2011 | [Eggers, Andreas]
Kruglov, Evgeny
[Kupferschmid, Stefan]
[Scheibler, Karsten]
[Teige, Teige]
Weidenbach, Christoph | | SUP(NLA) -- Combining Superposition and Non-Linear Arithmetic
In: 8th International Symposium on Frontiers of Combining Systems, 119-134 | Proceedings Article | |
| 2 |
| Tiwari, Ashish |
| |
| | 2011 | Sturm, Thomas
[Tiwari, Ashish] | | Verification and Synthesis Using Real Quantifier Elimination
In: ISSAC 2011 : Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation, 329-336 | Proceedings Article | |
| | 2010 | [Ghilardi, Silvio]
[Sattler, Ulrike]
Sofronie-Stokkermans, Viorica
[Tiwari, Ashish] | | Special issue on automated deduction: Decidability, complexity, tractability
In: Journal of Symbolic Computation [45], 151-152 | Journal Article | |
| 2 |
| |
| | 2009 | | | UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings | Electronic Proceedings | |
| | 2007 | | | Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07) | Proceedings | |
| 2 |
| Topic, Dalibor |
| |
| | 2007 | Weidenbach, Christoph
[Schmidt, Renate]
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor | | System Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520 | Proceedings Article | |
| | 2006 | Hillenbrand, Thomas
Topic, Dalibor
Weidenbach, Christoph | | Sudokus as Logical Puzzles
In: Disproving'06: Non-Theorems, Non-Validity, Non-Provability, 2-12 | Proceedings Article | |
| 3 |
| |
| | 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 | 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 | |
| 2 |
| |
| | 2009 | Tran, Duc-Khanh
[Ringeissen, Christopher]
[Ranise, Silvio]
[Kirchner, Helene] | | Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation
In: Journal of Symbolic Computation [45-], 261-286 | Journal Article | |
| | 2008 | [Lynch, Christopher]
Tran, Duc-Khanh | | SMELS: Satisfiability Modulo Equality with Lazy Superposition
In: Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008, 186-200 | Proceedings Article | |
| 2 |
| Turunen, Esko (ed.) |
| |
| | 2000 | [Iturrioz, Luisa]
Sofronie-Stokkermans, Viorica | | SHn-algebras (Symmetric Heyting algebras of order n)
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-11 | Part of a Book | |
| | 2000 | Sofronie-Stokkermans, Viorica | | Some properties of Kleene algebras
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-7 | Part of a Book | |
| 1 |
| |
| | 2007 | Sofronie-Stokkermans, Viorica | | Algebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493 | Part of a Book | |
| 1 |
| Vaz de Carvalho, Júlia (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 |
| |
| | 2010 | Burel, Guillaume | | Embedding Deduction Modulo into a Prover
In: Computer Science Logic : 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, 155-169 | 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 | |
| 1 |
| Viswanathan, Mahesh (ed.) |
| |
| | 2008 | [Lynch, Christopher]
Tran, Duc-Khanh | | SMELS: Satisfiability Modulo Equality with Lazy Superposition
In: Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008, 186-200 | Proceedings Article | |
| 1 |
| |
| | 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 |
| |
| | 2013 | [Kapur, Deepak]
[Nieuwenhuis, Robert]
[Voronkov, Andrei]
Weidenbach, Christoph
[Wilhelm, Reinhard] | | Harald Ganzinger's Legacy: Contributions to Logics and Programming
In: Programming Logics, | 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 | |
| 1 |
| Voronkov, Andrei Voronkov |
| |
| | 2013 | Voronkov, Andrei Voronkov
Weidenbach, Christoph | | Programming Logics - Essays in Memory of Harald Ganzinger | Book | |
| 15 |
| Voronkov, Andrei (ed.) |
| |
| | 2013 | Hillenbrand, Thomas
[Piskac, Ruzica]
Waldmann, Uwe
Weidenbach, Christoph | | From Search to Computation: Redundancy Criteria and Simplification at Work
In: Programming Logics, Essays in Memory of Harald Ganzinger, ? | Part of a Book | |
| | 2013 | [Kapur, Deepak]
[Nieuwenhuis, Robert]
[Voronkov, Andrei]
Weidenbach, Christoph
[Wilhelm, Reinhard] | | Harald Ganzinger's Legacy: Contributions to Logics and Programming
In: Programming Logics, | Proceedings Article | |
| | 2013 | Sofronie-Stokkermans, Viorica | | On combinations of local theory extensions
In: Programming Logics, Essays in Memory of Harald Ganzinger, 392-413 | Part of a Book | |
| | 2012 | Fietzke, Arnaud
Kruglov, Evgeny
Weidenbach, Christoph | | 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 | Proceedings Article | |
| | 2012 | Suda, Martin
Weidenbach, Christoph | | Labelled Superposition for PLTL
In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, 391-405 | Proceedings Article | |
| | 2010 | Horbach, Matthias | | Disunification for Ultimately Periodic Interpretations
In: Logic for Programming, Artificial Intelligence, and Reasoning : 16th International Conference, LPAR-16, 290-311 | Proceedings Article | |
| | 2010 | Fietzke, Arnaud
[Hermanns, Holger]
Weidenbach, Christoph | | Superposition-based Analysis of First-Order Probabilistic Timed Automata
In: Logic for Programming, Artificial Intelligence, and Reasoning : 17th International Conference, LPAR-17, 302-316 | Proceedings Article | |
| | 2007 | [Ludwig, Michel]
Waldmann, Uwe | | 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 | Proceedings Article | |
| | 2006 | Ganzinger, Harald
[Korovin, Konstantin] | | Theory Instantiation
In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06), 497-511 | Proceedings Article | |
| | 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 | |
| | 2002 | Hillenbrand, Thomas
[Löchner, Bernd] | | The Next WALDMEISTER Loop
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 486-500 | Proceedings Article | |
| | 2001 | Weidenbach, Christoph | | Combining Superposition, Sorts and Splitting
In: Handbook of Automated Reasoning, 1965-2013 | Part of a Book | |
| | 2001 | Nonnengart, Andreas
Weidenbach, Christoph | | Computing small clause normal forms
In: Handbook of Automated Reasoning, 335-367 | Part of a Book | |
| | 2001 | Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph | | First-Order Atom Definitions Extended
In: Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001), 309-319 | Proceedings Article | |
| | 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 | |
| 32 |
| Waldmann, Uwe |
| |
| | 2013 | Hillenbrand, Thomas
[Piskac, Ruzica]
Waldmann, Uwe
Weidenbach, Christoph | | From Search to Computation: Redundancy Criteria and Simplification at Work
In: Programming Logics, Essays in Memory of Harald Ganzinger, ? | Part of a Book | |
