| BibTeX cite key | Author/Editor | Year | | Title | Type |
|---|
| AfshordelHillenbrandWeidenbach01 | Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph | 2001 |  | 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 |
| AlthausEtAlFrocos2009 | Althaus, Ernst
Kruglov, Evgeny
Weidenbach, Christoph | 2009 | | Superposition Modulo Linear Arithmetic SUP(LA)
In: Frontiers of Combining Systems : 7th International Symposium, FroCoS 2009, 84-99 | Proceedings Article |
| AvenhausHillenbrandLoechner2003 | Avenhaus, Jürgen
Hillenbrand, Thomas
Löchner, Bernd | 2003 | | On Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233 | Journal Article |
| Azmy12 | Azmy, Noran | 2012 | | Formula Renaming with Generalizations
Universität des Saarlandes | Thesis - Masters thesis |
| BachmairGanzinger-94-jlc | Bachmair, Leo
Ganzinger, Harald | 1994 | | Rewrite-based equational theorem proving with selection and simplification
In: Journal of Logic and Computation [4], 217-247 | Journal Article |
| BachmairGanzingerWaldmann-92-alp | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | 1992 | | Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434 | Proceedings Article |
| BachmairGanzingerWaldmann-93-kgs | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | 1993 | | 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 |
| BachmairGanzingerWaldmann-93-lics | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | 1993 | | Set Constraints are the Monadic Class
In: Eighth Annual IEEE Symposium on Logic in Computer Science, 75-83 | Proceedings Article |
| BachmairGanzingerWaldmann-94-aaecc | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | 1994 | | Refutational Theorem Proving for Hierarchic First-Order Theories
In: Applicable Algebra in Engineering, Communication and Computing (AAECC) [5], 193-212 | Journal Article |
| Bankstahl06 | Bankstahl, Jan | 2006 | | Netflow analysis of SAP R/3 traffic in an enterprise environment
Universität des Saarlandes | Thesis - other |
| Bankstahl2006 | Bankstahl, Jan | 2006 | | Netflow analysis of SAP R/3 traffic in an enterprise
Universität des Saarlandes | Thesis - Masters thesis |
| Bastuck2006 | Bastuck, Andrea | 2006 | | Maschinell unterstützte Analyse eines Sicherheitsprotokolls
Universität des Saarlandes | Thesis - other |
| BaumgartnerWaldmann2009CADE | Baumgartner, Peter
Waldmann, Uwe | 2009 | | Superposition and Model Evolution Combined
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 17-34 | Proceedings Article |
| BaumgartnerWaldmann2011 | Baumgartner, Peter
Waldmann, Uwe | 2011 | | A Combined Superposition and Model Evolution Calculus
In: Journal of Automated Reasoning [47], 191-227 | Journal Article |
| Bromberger12 | Bromberger, Martin | 2012 | | Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic
Universität des Saarlandes | Thesis - Bachelor thesis |
| Burel2010 | Burel, Guillaume | 2010 | | 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 |
| Burel2010a | Burel, Guillaume | 2011 | | 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 |
| Damm-Ihlemann-Sofronie-Stokkermans2011 | Damm, Werner
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | 2011 | | 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 |
| Damm-Ihlemann-Sofronie-Stokkermans2011-msc | Damm, Werner
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | 2011 | | PTIME parametric verification of safety properties for reasonable linear hybrid automata
In: Mathematics in Computer Science [5], 469-497 | Journal Article |
| Damm-Ihlemann-Sofronie-Stokkermans2011-report | Damm, Werner
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | 2011 | | PTIME parametric verification of safety properties for reasonable linear hybrid automata | Report |
| DammDierksDischEtAl2011 | Damm, Werner
Dierks, Henning
Disch, Stefan
Hagemann, Willem
Pigorsch, Florian
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris | 2011 | | 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 |
| DammDierksDischEtAl2012 | Damm, Werner
Dierks, Henning
Disch, Stefan
Hagemann, Willem
Pigorsch, Florian
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris | 2012 | | Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
In: Science of Computer Programming [77], 1122-1150 | Journal Article |
| DammDierksHagemannEtAl2011 | Damm, Werner
Disch, Stefan
Hagemann, Willem
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris | 2011 | | Integrating incremental flow pipes into a symbolic model checker for hybrid systems | Report |
| DammDischHungarJacobsPangPigorschSchollWaldmannWirtz2007 | Damm, Werner
Disch, Stefan
Hungar, Hardi
Jacobs, Swen
Pang, Jun
Pigorsch, Florian
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris | 2007 | | 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 |
| DammDischHungarPangPigorschSchollWaldmannWirtz2006 | Damm, Werner
Disch, Stefan
Hungar, Hardi
Pang, Jun
Pigorsch, Florian
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris | 2006 | | 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 |
| Dhungana2013 | Dhungana, Deepak
Tang, Ching Hoo
Weidenbach, Christoph
Wischnewski, Patrick | 2013 | | Automated Verification of Interactive Rule-Based Configuration Systems
In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 551-561 | Proceedings Article |
| Dimova09 | Dimova, Dilyana | 2009 | | On the Translation of Timed Automata into First-order Logic
Universität des Saarlandes | Thesis - Masters thesis |
| Dimova2007 | Dimova, Dilyana | 2007 | | Propositional Abduction
Universität des Saarlandes | Thesis - Bachelor thesis |
| Dressler09 | Dreßler, Christian | 2009 | | Automatic Analysis of Tree-Based Feature Models with SPASS
Universität des Saarlandes | Thesis - Masters thesis |
| Dressler2007 | Dressler, Christian | 2007 | | First-Order Proof Documentation
Universität des Saarlandes | Thesis - Bachelor thesis |
| ErramiEiswirth:13a | Errami, H.
Eiswirth, M.
Grigoriev. D.
Seiler, W.
Sturm, T.
Weber, A. | 2013 | | Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates
In: Proceedings of the CASC 2013, 88-99 | Proceedings Article |
| Esquivel13 | Esquivel Pinto, Claudia So fia | 2013 | | Computing Variable Orders for SAT-Problems
Universität des Saarlandes | Thesis - Masters thesis |
| faber-ihlemann-jacobs-sofronie-2010-report | Faber, Johannes
Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica | 2010 | | Automatic Verification of Parametric Specifications with Complex Topologies | Report |
| faber-ihlemann-jacobs-sofronieStokkermans-ifm-2010 | Faber, Johannes
Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica | 2010 | | Automatic Verification of Parametric Specifications with Complex Topologies
In: Integrated Formal Methods : 8th International Conference, IFM 2010, 152-167 | Proceedings Article |
| faber-jacobs-sofronie-ifm-2007 | Faber, Johannes
Jacobs, Swen
Sofronie-Stokkermans, Viorica | 2007 | | Verifying CSP-OZ-DC specifications with complex data types and timing parameters
In: Proceedings of IFM 2007: Integrated Formal Methods, 233-252 | Proceedings Article |
| Fehreretal94a | Fehrer, Detlef
Hustadt, Ullrich
Jaeger, Manfred
Nonnengart, Andreas
Ohlbach, Hans Jürgen
Schmidt, Renate A.
Weidenbach, Christoph
Weydert, Emil | 1994 | | Description Logics for Natural Language Processing
In: International Workshop on Description Logics '94, 80-84 | Proceedings Article |
| Fietzke2007 | Fietzke, Arnaud | 2007 | | Labelled Splitting
Universität des Saarlandes | Thesis - Masters thesis |
| FietzkeKruglovWeidenbach2012 | Fietzke, Arnaud
Kruglov, Evgeny
Weidenbach, Christoph | 2012 | | 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 |
| FietzkeWeidenbach09 | Fietzke, Arnaud
Weidenbach, Christoph | 2009 | | Labelled Splitting
In: Annals of Mathematics and Artificial Intelligence [55], 3-34 | Journal Article |
| FietzkeWeidenbach2008 | Fietzke, Arnaud
Weidenbach, Christoph | 2008 | | Labelled Splitting | Report |
| FietzkeWeidenbach2010 | Fietzke, Arnaud
Hermanns, Holger
Weidenbach, Christoph | 2010 | | 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 |
| FietzkeWeidenbach2011 | Fietzke, Arnaud
Weidenbach, Christoph | 2011 | | Superposition as a Decision Procedure for Timed Automata
In: Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2011), | Proceedings Article |
| FietzkeWeidenbachCADE08 | Fietzke, Arnaud
Weidenbach, Christoph | 2008 | | Labelled Splitting
In: IJCAR, 459-474 | Proceedings Article |
| FietzkeWeidenbachMCS2012 | Fietzke, Arnaud
Weidenbach, Christoph | 2012 | | Superposition as a Decision Procedure for Timed Automata
In: Mathematics in Computer Science [6], 409-425 | Electronic Journal Article |
| FontaineMerzWeidenbach12 | Fontaine, Pascal
Merz, Stephan
Weidenbach, Christoph | 2012 | | Combination of Disjoint Theories: Beyond Decidability
In: Proceedings of the 6th International Joint Conference on Automated Reasoning, | Proceedings Article |
| Freiheit2005 | Freiheit, Jörn
Luuk, Marc
Münch, Susanne
Sijanski, Grozdana
Zangl, Fabrice | 2006 | | Lexecute: Visualisation and representation of legal procedures
In: Digital Evidence Journal [3], 17-27 | Journal Article |
| Freiheit2005b | Freiheit, Jörn
Zangl, Fabrice | 2006 | | Model-based user-interface management for public services
In: 6th European Conference on e-Government, 141-151 | Proceedings Article |
| Freiheit2005c | Lilith, Nimrod
Billington, Jonathan
Freiheit, Jörn | 2006 | | 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 |
| Freiheit2005d | Simon, Carlo
Freiheit, Jörn
Olbrich, Sebastian | 2006 | | Using BPEL processes defined by Event-driven Process Chains
In: 5. GI-Workshop "EPK 2006 - Geschäftsprozessmanagement mit Ereignisgesteuerten Prozessketten", 121-135 | Proceedings Article |
| Freiheit2007a | Freiheit, Jörn
Zangl, Fabrice | 2007 | | Model-based User-interface Management for Public Services
In: Electronic Journal of e-Government [5], 53-62 | Journal Article |
| Freiheit2007c | Ziemann, Joerg
Matheis, Thomas
Freiheit, Jörn | 2007 | | Modelling of Cross-Organizational Business Processes - Current Methods and Standards
In: Enterprise Modelling and Information Systems Architectures [2], 23-31 | Journal Article |
| Freiheit2007d | Ziemann, Joerg
Matheis, Thomas
Freiheit, Jörn | 2007 | | Modelling of Cross-Organizational Business Processes
In: Enterprise Modelling and Information Systems Architectures 2007, 87-95 | Proceedings Article |
| ftp09 | Peltier, Sofronie-Stokkermans (ed.) | 2009 | | First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving, Proceedings | Proceedings |
| GaillourdetHillenbrandLoechner2003 | Gaillourdet, Jean-Marie
Hillenbrand, Thomas
Löchner, Bernd
Spies, Hendrik | 2003 | | The New WALDMEISTER Loop at Work
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 317-321 | Proceedings Article |
| GanKor:ThInst:2006 | Ganzinger, Harald
Korovin, Konstantin | 2006 | | Theory Instantiation
In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06), 497-511 | Proceedings Article |
| Ganzinger-94-sat | Ganzinger, Harald | 1994 | | The Saturate System | Unpublished/Draft |
| Ganzinger-SofronieStokkermans-Waldmann-ijcar-2004 | Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Waldmann, Uwe | 2004 | | Modular Proof Systems for Partial Functions with Weak Equality
In: Automated reasoning : Second International Joint Conference, IJCAR 2004, 168-182 | Proceedings Article |
| GanzingerHillenbrandWaldmann2003 | Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe | 2003 | | Superposition modulo a Shostak Theory
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 182-196 | Proceedings Article |
| GanzingerKorovin-03-lics | Ganzinger, Harald
Korovin, Konstantin | 2003 | | New Directions in Instantiation-Based Theorem Proving
In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), 55-64 | Proceedings Article |
| GanzingerMeyerWeidenbach-97-cade | Ganzinger, Harald
Meyer, Christoph
Weidenbach, Christoph | 1997 | | Soft Typing for Ordered Resolution
In: Proceedings of the 14th International Conference on Automated Deduction (CADE-14), 321-335 | Proceedings Article |
| GanzingerSofronie-Stokkermans-00-ismvl | Ganzinger, Harald
Sofronie-Stokkermans, Viorica | 2000 | | 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 |
| GanzingerWaldmann-92-ctrs | Ganzinger, Harald
Waldmann, Uwe | 1992 | | 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 |
| GanzingerWaldmann1996CADE | Ganzinger, Harald
Waldmann, Uwe | 1996 | | Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 388-402 | Proceedings Article |
| Gasse-Sofronie-Stokkermans-dl2011 | Gasse, Francis
Sofronie-Stokkermans, Viorica | 2011 | | 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 |
| GSW-i-and-c | Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Waldmann, Uwe | 2006 | | Modular Proof Systems for Partial Functions with Evans Equality
In: Information and Computation [204], 1453-1492 | Journal Article |
| HaehnleKerberEtAl96 | Hähnle, Reiner
Kerber, Manfred
Weidenbach, Christoph | 1996 | | Common Syntax of the DFG-Schwerpunktprogramm ``Deduktion'' | Report |
| Hillenbrand2003 | Hillenbrand, Thomas | 2003 | | 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 |
| Hillenbrand2004 | Hillenbrand, Thomas | 2004 | | 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 |
| HillenbrandDiss2008 | Hillenbrand, Thomas | 2008 | | Superposition and Decision Procedures -- Back and Forth
Universität des Saarlandes | Thesis - PhD thesis |
| HillenbrandEtAl2006Disproving | Hillenbrand, Thomas
Topic, Dalibor
Weidenbach, Christoph | 2006 | | Sudokus as Logical Puzzles
In: Disproving'06: Non-Theorems, Non-Validity, Non-Provability, 2-12 | Proceedings Article |
| HillenbrandLoechner2001 | Hillenbrand, Thomas
Löchner, Bernd | 2001 | | The Next WALDMEISTER Loop (Extended Abstract)
In: Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001, 13-21 | Proceedings Article |
| HillenbrandPiskacWaldmannWeidenbach2011 | Hillenbrand, Thomas
Piskac, Ruzica
Waldmann, Uwe
Weidenbach, Christoph | 2013 | | From Search to Computation: Redundancy Criteria and Simplification at Work
In: Programming Logics, Essays in Memory of Harald Ganzinger, ? | Part of a Book |
| HillenbrandWeidenbach13 | Hillenbrand, Thomas
Weidenbach, Christoph | 2013 | | Superposition for Bounded Domains
In: Automated Reasoning and Mathematics, Essays in Memory of William W. McCune, 68-100 | Part of a Book |
| HillenbrandWeidenbach2007Report | Hillenbrand, Thomas
Weidenbach, Christoph | 2007 | | Superposition for Finite Domains | Report |
| Hirt2006 | Hirth, Simon | 2006 | | Automatische Analyse von DHCP und höheren Infrasturkturdiensten mit SPASS
Universität des Saarlandes | Thesis - Masters thesis |
| HirthKarlWeidenbach2007report | Hirth, Simon
Karl, Carsten
Weidenbach, Christoph | 2007 | | Automatic Analysis of LAN Infrastructures | Report |
| HL02-CADE18 | Hillenbrand, Thomas
Löchner, Bernd | 2002 | | The Next WALDMEISTER Loop
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 486-500 | Proceedings Article |
| Horbach2009TR1 | Horbach, Matthias
Weidenbach, Christoph | 2009 | | Deciding the Inductive Validity of Forall Exists* Queries | Report |
| Horbach2009TR2 | Horbach, Matthias
Weidenbach, Christoph | 2009 | | Superposition for Fixed Domains | Report |
| Horbach2010 | Horbach, Matthias | 2010 | | Disunification for Ultimately Periodic Interpretations
In: Logic for Programming, Artificial Intelligence, and Reasoning : 16th International Conference, LPAR-16, 290-311 | Proceedings Article |
| Horbach2010PhD | Horbach, Matthias | 2010 | | Superposition-based Decision Procedures for Fixed Domain and Minimal Model Semantics
Universität des Saarlandes | Thesis - PhD thesis |
| Horbach2013Informatik | Horbach, Matthias | 2013 | | INFORMATIK 2013 - Informatik angepasst an Mensch, Organisation und Umwelt | Book |
| Horbach2013McCune | Kapur, Deepak
Zhang, Zhihai
Horbach, Matthias
Zhao, Hantao
Lu, Qi
Nguyen, ThanhVu | 2014 | | 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 |
| HorbachWeidenbach2009CADE | Horbach, Matthias
Weidenbach, Christoph | 2009 | | Decidability Results for Saturation-Based Model Building
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 404-420 | Proceedings Article |
| HorbachWeidenbach2010 | Horbach, Matthias
Weidenbach, Christoph | 2010 | | Superposition for Fixed Domains
In: ACM Transactions on Computational Logic [11], 27,1-27,35 | Journal Article |
| HorbachWeidenbachCSL08 | Horbach, Matthias
Weidenbach, Christoph | 2008 | | Superposition for Fixed Domains
In: CSL, 293-307 | Proceedings Article |
| HorbachWeidenbachCSL09 | Horbach, Matthias
Weidenbach, Christoph | 2009 | | 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 |
| hpilot2009 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | 2009 | | System Description: H-PILoT
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 131-139 | Proceedings Article |
| HPT02 | Hillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor | 2002 | | 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 |
| HSW1998 | Hustadt, Ullrich
Schmidt, Renate A.
Weidenbach, Christoph | 1998 | | 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 |
| ihlemann-jacobs-sofronie-tacas2008 | Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica | 2008 | | On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281 | Proceedings Article |
| Ihlemann-Sofronie-Stokkermans-atr60-2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | 2010 | | On hierarchical reasoning in combinations of theories | Report |
| Ihlemann-Sofronie-Stokkermans-atr61-2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | 2010 | | System Description: H-PILoT (Version 1.9) | Report |
| Ihlemann-Sofronie-Stokkermans-ijcar-2010 | Ihlemann, Carsten
Sofronie-Stokkermans, Viorica | 2010 | | On Hierarchical Reasoning in Combinations of Theories
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 30-45 | Proceedings Article |
| IhlemannDiss2010 | Ihlemann, Carsten | 2010 | | Reasoning in Combinations of Theories
Universität des Saarlandes | Thesis - PhD thesis |
| jacobs-sofronie-pdpar-06 | Jacobs, Swen
Sofronie-Stokkermans, Viorica | 2006 | | 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 |
| jacobs-sofronie-pdpar-entcs | Jacobs, Swen
Sofronie-Stokkermans, Viorica | 2007 | | Applications of hierarchical reasoning in the verification of complex systems
In: Electronic Notes in Theoretical Computer Science [174], 39-54 | Electronic Journal Article |
| Jacobs2008 | Jacobs, Swen | 2008 | | Incremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62 | Proceedings Article |
| Jacobs2009 | Jacobs, Swen | 2009 | | Incremental Instance Generation in Local Reasoning
In: Computer Aided Verification : 21st International Conference, CAV 2009, 368-382 | Proceedings Article |
| JacobsDiss2010 | Jacobs, Swen | 2010 | | Hierarchic Decision Procedures for Verification
Universität des Saarlandes | Thesis - PhD thesis |
| JacobsWaldmann2005 | Jacobs, Swen
Waldmann, Uwe | 2005 | | Comparing Instance Generation Methods for Automated Reasoning
In: Automated Reasoning with Analytic Tableaux and Related Methods : International Conference, TABLEAUX 2005, 153-168 | Proceedings Article |
| JacobsWaldmann2006 | Jacobs, Swen
Waldmann, Uwe | 2006 | | Comparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78 | Electronic Journal Article |
| JacobsWaldmann2007 | Jacobs, Swen
Waldmann, Uwe | 2007 | | Comparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78 | Journal Article |
| JacquemardMeyerWeidenbach98 | Jacquemard, Florent
Meyer, Christoph
Weidenbach, Christoph | 1998 | | 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 |
| Karl2006 | Karl, Carsten | 2006 | | Automatische Analyse von Layer 3 Netzwerken mit SPASS
Universität des Saarlandes | Thesis - Masters thesis |
| KarrenbergKostaSturm2013 | Karrenberg, Ralf
Košta, Marek
Sturm, Thomas | 2013 | | Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70 | Proceedings Article |
| Kosta2013 | Košta, Marek | 2013 | | 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 |
| Kruglov2008 | Kruglov, Evgeny | 2008 | | Superposition Modulo Linear Arithmetic
Universität des Saarlandes | Thesis - Masters thesis |
| KruglovDiss13 | Kruglov, Evgeny | 2013 | | Superposition Modulo Theory
Universität des Saarlandes | Thesis - PhD thesis |
| KruglovFroCoS2011 | Eggers, Andreas
Kruglov, Evgeny
Kupferschmid, Stefan
Scheibler, Karsten
Teige, Teige
Weidenbach, Christoph | 2011 | | SUP(NLA) -- Combining Superposition and Non-Linear Arithmetic
In: 8th International Symposium on Frontiers of Combining Systems, 119-134 | Proceedings Article |
| KruglovMACIS2011 | Kruglov, Evgeny
Weidenbach, Christoph | 2011 | | 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 |
| KruglovWeidenbachMCS2012 | Kruglov, Evgeny
Weidenbach, Christoph | 2012 | | Superposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456 | Journal Article |
| KruglovWeidenbachMCS2012e | Kruglov, Evgeny
Weidenbach, Christoph | 2012 | | Superposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456 | Journal Article |
| Lamotte-SchubertWeidenbachFTP09 | Lamotte-Schubert, Manuel
Weidenbach, Christoph | 2009 | | 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 |
| Lamotte-SchubertWeidenbachFTP09CEUR | Lamotte-Schubert, Manuel
Weidenbach, Christoph | 2009 | | Analysis of Authorizations in SAP R/3
In: FTP 2009 : First-Order Theorem Proving, 90-104 | Electronic Proceedings Article |
| LAMOTTE2008 | Lamotte, Manuel | 2008 | | Analysis of Authorizations in SAP R/3
Fachhochschule Trier | Thesis - Masters thesis |
| LasarukSturm:11a | Lasaruk, Aless
Sturm, Thomas | 2011 | | 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 |
| LetzWeidenbach98 | Letz, Reinhold
Weidenbach, Christoph | 1998 | | 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 |
| LevAmiWeidenbachEtAl2007CADE | Lev-Ami, Tal
Weidenbach, Christoph
Reps, Thomas
Sagiv, Mooly | 2007 | | Labelled Clauses
In: 21st International Conference on Automated Deduction (CADE-21), 311-327 | Proceedings Article |
| LoechnerHillenbrandAICOM2002 | Löchner, Bernd
Hillenbrand, Thomas | 2002 | | A Phytography of WALDMEISTER
In: AI Communications [15], 127-133 | Journal Article |
| LuDiss13 | Lu, Tianxiang | 2013 | | Formal Verification of the Pastry Protocol
Universität des Saarlandes | Thesis - PhD thesis |
| LudwigDipl2006 | Ludwig, Michel | 2006 | | Extensions of the Knuth-Bendix Ordering with LPO-like Properties
Universität des Saarlandes | Thesis - Masters thesis |
| LudwigWaldmann2007 | Ludwig, Michel
Waldmann, Uwe | 2007 | | 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 |
| LuTlaPastryForte2011 | Lu, Tianxiang
Merz, Stephan
Weidenbach, Christoph | 2011 | | 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 |
| LuTX2009 | Lu, Tianxiang
Merz, Stephan
Weidenbach, Christoph | 2010 | | Model Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21 | Proceedings Article |
| Neumann09 | Neumann, Stephan Rouven | 2009 | | Automated Proof Generation of Possibiltiy Properties in Inductive Protocol Verification
Universität des Saarlandes | Thesis - Bachelor thesis |
| NieuwenhuisHillenbrandRiazanovVoronkov2001 | Nieuwenhuis, Robert
Hillenbrand, Thomas
Riazanov, Alexandre
Voronkov, Andrei | 2001 | | On the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271 | Proceedings Article |
| NonnengartRockWeidenbach98 | Nonnengart, Andreas
Rock, Georg
Weidenbach, Christoph | 1998 | | On Generating Small Clause Normal Forms
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 397-411 | Proceedings Article |
| NonnengartWeidenbach2001handbook | Nonnengart, Andreas
Weidenbach, Christoph | 2001 | | Computing small clause normal forms
In: Handbook of Automated Reasoning, 335-367 | Part of a Book |
| OhlbachWeidenbach95 | Ohlbach, Hans Jürgen
Weidenbach, Christoph | 1995 | | A Note on Assumptions about Skolem Functions
In: Journal of Automated Reasoning [15], 267-275 | Journal Article |
| Peltier-Sofronie-Stokkermans-ftpceur-2010 | Peltier, Sofronie-Stokkermans (ed.) | 2009 | | First-Order Theorem Proving 2009 | Proceedings |
| PrevostoWaldmann2006 | Prevosto, Virgile
Waldmann, Uwe | 2006 | | SPASS+T
In: ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 18-33 | Proceedings Article |
| Reuter13 | Reuter, Jochen | 2013 | | Real Linear Quantifier Elimination
Universität des Saarlandes | Thesis - Masters thesis |
| RusevMaster2008 | Rusev, Rostislav | 2008 | | Bitvector Reasoning with SPASS
Universität des Saarlandes | Thesis - Masters thesis |
| Rybalchenko-Sofronie-Stokkermans-2009 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | 2009 | | Constraint Solving for Interpolation | Report |
| Rybalchenko-Sofronie-vmcai07 | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | 2007 | | Constraint Solving for Interpolation
In: Verification, Model Checking and Abstract Interpretation : 8th International Conference, VMCAI 2007, 346-362 | Proceedings Article |
| Sofronie-cade-05 | Sofronie-Stokkermans, Viorica | 2005 | | Hierarchic reasoning in local theory extensions
In: Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 219-234 | Proceedings Article |
| Sofronie-getco06-entcs | Sofronie-Stokkermans, Viorica | 2009 | | 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 |
| sofronie-ihlemann-ismvl-2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten | 2007 | | Automated reasoning in some local extensions of ordered structures
In: Proceedings of ISMVL 2007, Article1 | Proceedings Article |
| Sofronie-Ihlemann-Jacobs-dagstuhl07 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Jacobs, Swen | 2007 | | Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
In: Deduction and Decision Procedures, 1-22 | Electronic Proceedings Article |
| sofronie-ihlemann-jmvl-2007 | Sofronie-Stokkermans, Viorica
Ihlemann, Carsten | 2007 | | Automated reasoning in some local extensions of ordered structures
In: Journal of Multiple-Valued Logic and Soft Computing [13], 397-414 | Journal Article |
| Sofronie-ijcar-06 | Sofronie-Stokkermans, Viorica | 2006 | | Interpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250 | Proceedings Article |
| Sofronie-Stokkermans-2010-jsc | Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica | 2010 | | Constraint Solving for Interpolation
In: Journal of Symbolic Computation [45], 1212-1233 | Journal Article |
| Sofronie-Stokkermans-2013 | Sofronie-Stokkermans, Viorica | 2013 | | 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 |
| Sofronie-Stokkermans-addct07 | Ghilardi, Sattler, Sofronie-Stokkermans, Tiwari (ed.) | 2007 | | Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07) | Proceedings |
| Sofronie-Stokkermans-aiml2008 | Sofronie-Stokkermans, Viorica | 2008 | | 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 |
| Sofronie-Stokkermans-atr45-2008 | Sofronie-Stokkermans, Viorica | 2008 | | Efficient Hierarchical Reasoning about Functions over Numerical Domains | Report |
| Sofronie-Stokkermans-atr46-2008 | Sofronie-Stokkermans, Viorica | 2008 | | Sheaves and geometric logic and applications to modular verification of complex systems | Report |
| Sofronie-Stokkermans-cade-2011 | Bjørner, Sofronie-Stokkermans (ed.) | 2011 | | Automated Deduction - CADE-23 : 23rd International Conference on Automated Deduction | Proceedings |
| Sofronie-Stokkermans-cade09 | Sofronie-Stokkermans, Viorica | 2009 | | 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 |
| Sofronie-Stokkermans-cade2000 | Sofronie-Stokkermans, Viorica | 2000 | | On unification for bounded distributive lattices
In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), 465-481 | Proceedings Article |
| Sofronie-Stokkermans-cedar2008 | Baader, Ghilardi, Hermann, Sattler, Sofronie-Stokkermans (ed.) | 2008 | | Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08) | Proceedings |
| Sofronie-Stokkermans-ceur2010 | Peltier, Sofronie-Stokkermans (ed.) | 2010 | | First-Order Theorem Proving : Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09) | Electronic Proceedings |
| Sofronie-Stokkermans-dagstuhl-2010 | Sofronie-Stokkermans, Viorica | 2010 | | 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 |
| Sofronie-Stokkermans-dam-06 | Sofronie-Stokkermans, Viorica | 2007 | | Automated theorem proving by resolution in non-classical logics
In: Annals of Mathematics and Artificial Intelligence [49], 221-252 | Journal Article |
| Sofronie-Stokkermans-dl2008 | Sofronie-Stokkermans, Viorica | 2008 | | 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 |
| Sofronie-Stokkermans-dualities1999 | Sofronie-Stokkermans, Viorica | 1999 | | Priestley representation for distributive lattices with operators and applications to automated theorem proving
In: Dualities, Interpretability and Ordered Structures, 43-54 | Proceedings Article |
| Sofronie-Stokkermans-esslli09 | Sofronie-Stokkermans, Viorica | 2009 | | Reasoning in Complex Theories and Applications. Advanced Lecture
In: ESSLLI 2009 : European Summer School in Logic, Language and Information, 1-64 | Electronic Proceedings Article |
| Sofronie-Stokkermans-frocos-07 | Sofronie-Stokkermans, Viorica | 2007 | | 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 |
| Sofronie-Stokkermans-frocos-2011 | Tinelli, Sofronie-Stokkermans (ed.) | 2011 | | Frontiers of Combining Systems | Proceedings |
| Sofronie-Stokkermans-frocos2013 | Horbach, Matthias
Sofronie-Stokkermans, Viorica | 2013 | | Obtaining Finite Local Theory Axiomatizations via Saturation
In: Frontiers of Combining Systems - 9th International Symposium, 198-213 | Proceedings Article |
| Sofronie-Stokkermans-ftp07-abstract | Sofronie-Stokkermans, Viorica | 2007 | | 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 |
| Sofronie-Stokkermans-ftp2000 | Sofronie-Stokkermans, Viorica | 2000 | | 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 |
| Sofronie-Stokkermans-getco-06 | Sofronie-Stokkermans, Viorica | 2006 | | Sheaves and geometric logic in concurrency
In: Proceedings of the Eighth Workshop on Geometric and Topological Methods in Concurrency (GETCO 2006), ? | Proceedings Article |
| Sofronie-Stokkermans-hab04 | Sofronie-Stokkermans, Viorica | 2004 | | Algebraic and logical methods in automated theorem proving and in the study of concurrency
Universität des Saarlandes | Thesis - Habilitation thesis |
| Sofronie-Stokkermans-ismvl-2004 | Sofronie-Stokkermans, Viorica | 2004 | | 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 |
| Sofronie-Stokkermans-jahrbuch-2006 | Sofronie-Stokkermans, Viorica | 2006 | | Automatisches Beweisen in komplexen Theorien
In: MPG Jahrbuch [-], | Electronic Journal Article |
| Sofronie-Stokkermans-jim-2003 | Sofronie-Stokkermans, Viorica | 2003 | | 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 |
| Sofronie-Stokkermans-ki2008 | Sofronie-Stokkermans, Viorica | 2008 | | Efficient hierarchical reasoning about functions over numerical domains
In: KI 2008: Advances in Artificial Intelligence, 135-143 | Proceedings Article |
| Sofronie-Stokkermans-lmcs-2008 | Sofronie-Stokkermans, Viorica | 2008 | | Interpolation in local theory extensions
In: Logical Methods in Computer Science [4], 31 pages | Electronic Journal Article |
| Sofronie-Stokkermans-moisil-08 | Sofronie-Stokkermans, Viorica | 2007 | | Algebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493 | Part of a Book |
| Sofronie-Stokkermans-mvl-2003 | Sofronie-Stokkermans, Viorica | 2003 | | 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 |
| Sofronie-Stokkermans-sacs2013 | Sofronie-Stokkermans, Viorica | 2013 | | Locality and Applications to Subsumption Testing in EL and Some of its Extensions
In: Scientific Annals of Computer Science [23], 251-284 | Journal Article |
| Sofronie-Stokkermans-tableaux-2002 | Sofronie-Stokkermans, Viorica | 2002 | | 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 |
| Sofronie-Stokkermans-tutorial-ki08 | Sofronie-Stokkermans, Viorica | 2008 | | Reasoning in Complex Theories and Applications | Miscellaneous |
| Sofronie-Stokkermans-unif-05 | Sofronie-Stokkermans, Viorica | 2007 | | On unification for bounded distributive lattices
In: ACM Transactions on Computational Logic [8], 12.1-12.28 | Journal Article |
| Sofronie-Stokkermans1999 | Sofronie-Stokkermans, Viorica | 2001 | | 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 |
| Sofronie-Stokkermans1999-cade | Sofronie-Stokkermans, Viorica | 1999 | | 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 |
| Sofronie-Stokkermans1999-fct | Sofronie-Stokkermans, Viorica
Stokkermans, Karel | 1999 | | Modeling Interaction by Sheaves and Geometric Logic
In: Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99), 512-523 | Proceedings Article |
| Sofronie-Stokkermans1999-ismvl | Sofronie-Stokkermans, Viorica | 1999 | | 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 |
| Sofronie-Stokkermans1999-lmps | Sofronie-Stokkermans, Viorica | 1999 | | 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 |
| Sofronie-Stokkermans2000-atlas-1 | Iturrioz, Luisa
Sofronie-Stokkermans, Viorica | 2000 | | 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 |
| Sofronie-Stokkermans2000-atlas-2 | Sofronie-Stokkermans, Viorica | 2000 | | 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 |
| Sofronie-Stokkermans2001-ismvl | Sofronie-Stokkermans, Viorica | 2001 | | 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 |
| Sofronie-Stokkermans2006 | Sofronie-Stokkermans, Viorica | 2007 | | 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 |
| Sofronie-Stokkermans2009-addct-unif | Lynch, Narendran, Baader, Ghilardi, Hermann, Sofronie-Stokkermans, Tiwari (ed.) | 2009 | | UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings | Electronic Proceedings |
| Sofronie-Stokkermans2009-jsc-addct | Ghilardi, Silvio
Sattler, Ulrike
Sofronie-Stokkermans, Viorica
Tiwari, Ashish | 2010 | | Special issue on automated deduction: Decidability, complexity, tractability
In: Journal of Symbolic Computation [45], 151-152 | Journal Article |
| Sofronie-Stokkermans2010-ijcar | Sofronie-Stokkermans, Viorica | 2010 | | Hierarchical Reasoning for the Verification of Parametric Systems
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 171-187 | Proceedings Article |
| Sofronie-Stokkermans2012-jsc-ftp | Peltier, Nicolas
Sofronie-Stokkermans, Viorica | 2012 | | First-order theorem proving: Foreword
In: Journal of Symbolic Computation [47], 1009-1010 | Journal Article |
| Sofronie-Stokkermans2013-jar-cade-special-issue | Bjorner, Nikolaj
Sofronie-Stokkermans, Viorica | 2013 | | Preface: Special Issue of Selected Extended Papers of CADE-23
In: Journal of Automated Reasoning [51], 1-2 | Journal Article |
| Sofronie-verify-06 | Sofronie-Stokkermans, Viorica | 2006 | | Local reasoning in verification
In: IJCAR'06 Workshop : VERIFY'06: Verification Workshop, 128-145 | Electronic Proceedings Article |
| Sofronie-wlphg11 | Sofronie-Stokkermans, Viorica | 2013 | | On combinations of local theory extensions
In: Programming Logics, Essays in Memory of Harald Ganzinger, 392-413 | Part of a Book |
| Sofronie1997a | Sofronie-Stokkermans, Viorica | 2000 | | 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 |
| Sofronie1997b | Sofronie-Stokkermans, Viorica | 2000 | | 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 |
| Sofronie1997c | Sofronie-Stokkermans, Viorica | 2000 | | 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 |
| Sofronie1998a | Sofronie-Stokkermans, Viorica | 1998 | | 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 |
| Sofronie1998b | Sofronie-Stokkermans, Viorica | 1998 | | Resolution-based Theorem Proving for SHn-Logics | Report |
| Sofronie1998c | Sofronie-Stokkermans, Viorica | 1998 | | 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 |
| SturmTiwari:11a | Sturm, Thomas
Tiwari, Ashish | 2011 | | 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 |
| SturmZengler2011 | Sturm, Zengler (ed.) | 2011 | | Automated Deduction in Geometry : 7th International Workshop, ADG 2008 | Proceedings |
| Suda2010 | Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick | 2010 | | On the Saturation of YAGO | Report |
| SudaSutcliffeWischnewskiLamotteKI2009 | Suda, Martin
Sutcliffe, Geoff
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard | 2009 | | External Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288 | Proceedings Article |
| SudaWeidenbachIJCAR2012 | Suda, Martin
Weidenbach, Christoph | 2012 | | A PLTL-prover based on labelled superposition with partial model guidance
In: Automated Reasoning : 6th International Joint Conference, IJCAR 2012, 537-543 | Proceedings Article |
| SudaWeidenbachLPAR2012 | Suda, Martin
Weidenbach, Christoph | 2012 | | Labelled Superposition for PLTL
In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, 391-405 | Proceedings Article |
| SudaWeidenbachWischnewskiIJCAR10 | Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick | 2010 | | On the Saturation of YAGO
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 441-456 | Proceedings Article |
| Teucke13 | Teucke, Andreas | 2013 | | CDCL with Reduction
Universität des Saarlandes | Thesis - Masters thesis |
| tran-atva08 | Lynch, Christopher
Tran, Duc-Khanh | 2008 | | SMELS: Satisfiability Modulo Equality with Lazy Superposition
In: Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008, 186-200 | Proceedings Article |
| tran-decproc-jsc | Tran, Duc-Khanh
Ringeissen, Christopher
Ranise, Silvio
Kirchner, Helene | 2009 | | Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation
In: Journal of Symbolic Computation [45-], 261-286 | Journal Article |
| VoronkovetAl13 | Kapur, Deepak
Nieuwenhuis, Robert
Voronkov, Andrei
Weidenbach, Christoph
Wilhelm, Reinhard | 2013 | | Harald Ganzinger's Legacy: Contributions to Logics and Programming
In: Programming Logics, | Proceedings Article |
| VoronkovWeidenbach13 | Voronkov, Andrei Voronkov
Weidenbach, Christoph | 2013 | | Programming Logics - Essays in Memory of Harald Ganzinger | Book |
| Waldmann1997 | Waldmann, Uwe | 1997 | | Cancellative Abelian Monoids in Refutational Theorem Proving
Universität des Saarlandes | Thesis - PhD thesis |
| Waldmann1997FTP | Waldmann, Uwe | 1997 | | 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 |
| Waldmann1998 | Waldmann, Uwe | 1998 | | Superposition for Divisible Torsion-Free Abelian Groups
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 144-159 | Proceedings Article |
| Waldmann1998IPL | Waldmann, Uwe | 1998 | | Extending reduction orderings to ACU-compatible reduction orderings
In: Information Processing Letters [67], 43-49 | Journal Article |
| Waldmann1999LPAR | Waldmann, Uwe | 1999 | | 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 |
| Waldmann2001IJCAR | Waldmann, Uwe | 2001 | | Superposition and Chaining for Totally Ordered Divisible Abelian Groups (Extended Abstract)
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 226-241 | Proceedings Article |
| Waldmann2002aJSC | Waldmann, Uwe | 2002 | | Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I)
In: Journal of Symbolic Computation [33], 777-829 | Journal Article |
| Waldmann2002bJSC | Waldmann, Uwe | 2002 | | Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II)
In: Journal of Symbolic Computation [33], 831-861 | Journal Article |
| Waldmann2002IUC | Waldmann, Uwe | 2002 | | A New Input Technique for Accented Letters in Alphabetical Scripts
In: Proceedings of the 20th International Unicode Conference, C12 | Proceedings Article |
| Waldmann92a | Waldmann, Uwe | 1992 | | Semantics of Order-Sorted Specifications
In: Theoretical Computer Science [94], 1-35 | Journal Article |
| Wand2012 | Blanchette, Jasmin Christian
Popescu, Andrei
Wand, Daniel
Weidenbach, Christoph | 2012 | | More SPASS with Isabelle : Superposition with Hard Sorts and Configurable Simplification
In: Interactive Theorem Proving : Third International Conference, ITP 2012, 345-360 | Proceedings Article |
| WBH+02-CADE18 | Weidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor | 2002 | | SPASS Version 2.0
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 275-279 | Proceedings Article |
| WeberSturm:11a | Weber, Andreas
Sturm, Thomas
Abdel-Rahman, Essam O. | 2011 | | Algorithmic Global Criteria for Excluding Oscillations
In: Bulletin of Mathematical Biology [73], 899-916 | Journal Article |
| Weidenbach1999jar | Weidenbach, Christoph | 1999 | | SPASS V0.95TPTP
In: Journal of Automated Reasoning [23], 21-21 | Journal Article |
| Weidenbach2000habil | Weidenbach, Christoph | 2000 | | Entscheidbarkeitsprobleme für monadische (Horn)Klauselklassen
Universität des Saarlandes, Naturwissenschaftlich-Technische Fakultät | Thesis - Habilitation thesis |
| Weidenbach2001handbook | Weidenbach, Christoph | 2001 | | Combining Superposition, Sorts and Splitting
In: Handbook of Automated Reasoning, 1965-2013 | Part of a Book |
| Weidenbach92a | Weidenbach, Christoph | 1993 | | A New Sorted Logic
In: GWAI-92: Advances in Artificial Inteligence, Proceedings 16th German Workshop on Artificial Intelligence, 43-54 | Proceedings Article |
| Weidenbach93a | Weidenbach, Christoph | 1993 | | Extending the Resolution Method with Sorts
In: Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI '93), 60-65 | Proceedings Article |
| Weidenbach94a | Weidenbach, Christoph | 1994 | | First-Order Tableaux with Sorts
In: TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 247-261 | Proceedings Article |
| Weidenbach94c | Weidenbach, Christoph | 1994 | | Sorts, Resolution, Tableaux and Propositional Logic
In: KI-94 Workshops: Extended Abstracts, 315-316 | Proceedings Article |
| Weidenbach95d | Weidenbach, Christoph | 1995 | | First-Order Tableaux with Sorts
In: Journal of the Interest Group in Pure and Applied Logics [3], 887-906 | Journal Article |
| Weidenbach95e | Barth, Peter
Kleine Büning, Hans
Weidenbach, Christoph | 1995 | | Workshop CPL Computational Propositional Logic
In: KI-95 Activities: Workshops, Posters, Demos, 71-72 | Proceedings Article |
| Weidenbach96a | Weidenbach, Christoph | 1996 | | Unification in Pseudo-Linear Sort Theories is Decidable
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 343-357 | Proceedings Article |
| Weidenbach96b | Weidenbach, Christoph
Gaede, Bernd
Rock, Georg | 1996 | | SPASS & FLOTTER, Version 0.42
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 141-145 | Proceedings Article |
| Weidenbach96c | Weidenbach, Christoph | 1996 | | Unification in Sort Theories
In: Proceedings of the 10th International Workshop on Unification, UNIF'96, 16-25 | Proceedings Article |
| Weidenbach96d | Weidenbach, Christoph | 1996 | | 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 |
| Weidenbach96e | Weidenbach, Christoph | 1996 | | Computational Aspects of a First-Order Logic with Sorts
Universität des Saarlandes | Thesis - PhD thesis |
| Weidenbach96f | Weidenbach, Christoph | 1996 | | Unification in Sort Theories and its Applications
In: Annals of Mathematics and Artificial Intelligence [18], 261-293 | Journal Article |
| Weidenbach97jar | Weidenbach, Christoph | 1997 | | SPASS Version 0.49
In: Journal of Automated Reasoning [18], 247-252 | Journal Article |
| Weidenbach98kluwer | Weidenbach, Christoph | 1998 | | Sorted Unification and Tree Automata
In: Automated Deduction - A Basis for Applications, 291-320 | Part of a Book |
| Weidenbach98teubner | Weidenbach, Christoph | 1998 | | Rechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197 | Part of a Book |
| Weidenbach99cade | Weidenbach, Christoph | 1999 | | 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 |
| Weidenbach99cadespass | Weidenbach, Christoph
Afshordel, Bijan
Brahm, Uwe
Cohrs, Christian
Engel, Thorsten
Keen, Enno
Theobalt, Christian
Topić, Dalibor | 1999 | | System Description: SPASS Version 1.0.0
In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 314-318 | Proceedings Article |
| WeidenbachEtAlSpass2009 | Weidenbach, Christoph
Dimova, Dilyana
Fietzke, Arnaud
Suda, Martin
Wischnewski, Patrick | 2009 | | SPASS Version 3.5
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 140-145 | Proceedings Article |
| WeidenbachMeyerEtAl98jar | Weidenbach, Christoph
Meyer, Christoph
Cohrs, Christian
Engel, Thorsten
Keen, Enno | 1998 | | SPASS V0.77
In: Journal of Automated Reasoning [21], 113-113 | Journal Article |
| WeidenbachSchmidtEtAl2007cade | Weidenbach, Christoph
Schmidt, Renate
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor | 2007 | | System Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520 | Proceedings Article |
| WeidenbachWischnewski2012 | Weidenbach, Christoph
Wischnewski, Patrick | 2012 | | Satisfiability Checking and Query Answering for large Ontologies
In: PAAR-2012 : Third Workshop on Practical Aspects of Automated Reasoning, 163-177 | Electronic Proceedings Article |
| WeidenbachWischnewskiAICom10 | Weidenbach, Christoph
Wischnewski, Patrick | 2010 | | Subterm Contextual Rewriting
In: AI Communications [23], 97-109 | Journal Article |
| WeidenbachWischnewskiCADE08 | Weidenbach, Christoph
Wischnewski, Patrick | 2008 | | Contextual Rewriting in SPASS
In: PAAR/ESHOL, 115-124 | Proceedings Article |
| WeidenbachWischnewskiReport2009 | Weidenbach, Christoph
Wischnewski, Patrick | 2009 | | Contextual Rewriting | Report |
| Wischnewski12 | Wischnewski, Patrick | 2012 | | Efficient Reasoning Procedures for Complex First-Order Theories
Universität des Saarlandes | Thesis - PhD thesis |
| Wischnewski2007 | Wischnewski, Patrick | 2007 | | Contextual Rewriting in SPASS
Universität des Saarlandes | Thesis - Masters thesis |
| Zimmer2007 | Zimmer, Stephan | 2007 | | Intelligent Combination of a First Order Theorem Prover and SMT Procedures
Universität des Saarlandes | Thesis - other |
