Filename | Size (KB) | Access | Type | Author(s) [non member] | Title | Year |
|---|
| _03LICS.pdf | 136 | Public
| Proceedings Article | 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 | 2003 |
| _03CADE.2.ps | 211 | Public
| Proceedings Article | Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe | Superposition modulo a Shostak Theory
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 182-196 | 2003 |
| _00ISMVL_ps.gz | 55 | Public
| Proceedings Article | 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 | 2000 |
| wm.ps | 393 | Intranet
| Journal Article | [Löchner, Bernd]
Hillenbrand, Thomas | A Phytography of WALDMEISTER
In: AI Communications [15], 127-133 | 2002 |
| wmloop.ps | 386 | Public
| Proceedings Article | Hillenbrand, Thomas
[Löchner, Bernd] | The Next WALDMEISTER Loop
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 486-500 | 2002 |
| Weidenbach.pdf | 269 | Internal
| Proceedings Article | 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 | 2007 |
| veiaspass.pdf | 762 | Public
| Thesis - Master's thesis | Dreßler, Christian | Automatic Analysis of Tree-Based Feature Models with SPASS
Universität des Saarlandes | 2009 |
| thesis.pdf | 278 | Intranet
| Thesis - Master's thesis | Fietzke, Arnaud | Labelled Splitting
Universität des Saarlandes | 2007 |
| thesis.pdf | 802 | Intranet
| Thesis - Diploma thesis | Zimmer, Stephan | Intelligent Combination of a First Order Theorem Prover and SMT Procedures
Universität des Saarlandes | 2007 |
| Thesis-Complete.pdf | 805 | Internal
| Thesis - Master's thesis | Azmy, Noran | Formula Renaming with Generalizations
Universität des Saarlandes | 2012 |
| tableaux-2002.pdf | 241 | Public
| Proceedings Article | 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 | 2002 |
| superpositionLTL.pdf | 465 | Internal
| Proceedings Article | Suda, Martin
Weidenbach, Christoph | Labelled Superposition for PLTL
In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, 391-405 | 2012 |
| superFixDom_TR.pdf | 333 | Public
| Report | Horbach, Matthias
Weidenbach, Christoph | Superposition for Fixed Domains | 2009 |
| SupDec.pdf | 952 | Public
| Thesis - Doctoral dissertation | Hillenbrand, Thomas | Superposition and Decision Procedures -- Back and Forth
Universität des Saarlandes | 2008 |
| studia-logica-2000-2.pdf | 1351
807 | Intranet
| Journal Article | 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 | 2000 |
| studia-logica-2000-1.pdf | 1351 | Intranet
| Journal Article | 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 | 2000 |
| studia-logica-2000-1.pdf | 1351
807 | Intranet
| Journal Article | 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 | 2000 |
| spass2002.ps | 106 | Public
| Proceedings Article | 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 | 2002 |
| sofronie-stokkermans-fct-1999.ps.gz | 92 | Public
| Proceedings Article | 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 | 1999 |
| sofronie-ijcar-06.pdf | 192 | Public
| Proceedings Article | Sofronie-Stokkermans, Viorica | Interpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250 | 2006 |
| sofronie-dam-revised.ps | 553 | Intranet
| Journal Article | Sofronie-Stokkermans, Viorica | Automated theorem proving by resolution in non-classical logics
In: Annals of Mathematics and Artificial Intelligence [49], 221-252 | 2007 |
| sofronie-cade2000.ps | 260 | Public
| Proceedings Article | Sofronie-Stokkermans, Viorica | On unification for bounded distributive lattices
In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), 465-481 | 2000 |
| sofronie-cade-2005.pdf | 518 | Public
| Proceedings Article | Sofronie-Stokkermans, Viorica | Hierarchic reasoning in local theory extensions
In: Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 219-234 | 2005 |
| sofronie-acm-tocl-final.pdf | 427 | Intranet
| Journal Article | Sofronie-Stokkermans, Viorica | On unification for bounded distributive lattices
In: ACM Transactions on Computational Logic [8], 12.1-12.28 | 2007 |
| SimonHirth.pdf | 402 | Intranet
| Thesis - Master's thesis | Hirth, Simon | Automatische Analyse von DHCP und höheren Infrasturkturdiensten mit SPASS
Universität des Saarlandes | 2006 |
| SapR3.pdf | 300 | Public
| Proceedings Article | 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 | 2009 |
| Quantifier_Elimination.pdf | 656 | Internal
| Thesis - Master's thesis | Reuter, Jochen | Real Linear Quantifier Elimination
Universität des Saarlandes | 2013 |
| pwm.ps | 110 | Public
| Proceedings Article | [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 | 2003 |
| proofdoc.pdf | 371 | Intranet
| Thesis - Bachelor thesis | [Dressler, Christian] | First-Order Proof Documentation
Universität des Saarlandes | 2007 |
| NOSup.ps | 104 | Public
| Electronic Proceedings Article | 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 | 2004 |
| next-wm-loop.ps | 244 |
| Proceedings Article | 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 | 2001 |
| mvl-book-02.ps | 375 | Public
| Part of a Book | 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 | 2003 |
| MPI-I-2008-RG1-001.pdf | 319 | Intranet
| Report | Hirth, Simon
Karl, Carsten
Weidenbach, Christoph | Automatic Analysis of LAN Infrastructures | 2007 |
| MPI-I-2008-RG1-001.pdf | 361 | Public
| Report | Fietzke, Arnaud
Weidenbach, Christoph | Labelled Splitting | 2008 |
| MPI-I-2007-RG1-002.pdf | 262 | Intranet
| Report | Hillenbrand, Thomas
Weidenbach, Christoph | Superposition for Finite Domains | 2007 |
| mcpastry-lu-avocs2010.pdf | 98 | Public
| Proceedings Article | 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 | 2010 |
| master.pdf | 339 | Intranet
| Thesis - Master's thesis | Wischnewski, Patrick | Contextual Rewriting in SPASS
Universität des Saarlandes | 2007 |
| master.pdf | 1341 | Intranet
| Thesis - Master's thesis | Lamotte, Manuel | Analysis of Authorizations in SAP R/3
Fachhochschule Trier | 2008 |
| MasterThesis.pdf | 465 | Intranet
| Thesis - Master's thesis | Rusev, Rostislav | Bitvector Reasoning with SPASS
Universität des Saarlandes | 2008 |
| ki2009.pdf | 167 | Public
| Proceedings Article | 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 | 2009 |
| jim-03-sofronie.ps.gz | 126 | Public
| Proceedings Article | 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 | 2003 |
| j-mvl-2001.ps.gz | 221 | Intranet
| Journal Article | 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 | 2001 |
| j-mvl-2000.ps | 337 | Intranet
| Journal Article | 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 | 2000 |
| InstGen.pdf | 196 | Intranet
| Electronic Journal Article | Jacobs, Swen
Waldmann, Uwe | Comparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78 | 2006 |
| InstGen.pdf | 196 | Intranet
| Journal Article | Jacobs, Swen
Waldmann, Uwe | Comparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78 | 2007 |
| InstGen-final.pdf | 428 | Public
| Proceedings Article | 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 | 2005 |
| ijcar2012_submission_81.pdf | 389 | Internal
| Proceedings Article | 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 | 2012 |
| IIGLR.pdf | 200 | Public
| Proceedings Article | Jacobs, Swen | Incremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62 | 2008 |
| IIGLR.pdf | 209 | Public
| Proceedings Article | Jacobs, Swen | Incremental Instance Generation in Local Reasoning
In: Computer Aided Verification : 21st International Conference, CAV 2009, 368-382 | 2009 |
| gjoin.ps | 264 | Public
| Journal Article | [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 | 2003 |
| ftp98-lncs-selection.pdf | 253 | Public
| Proceedings Article | 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 | 2000 |
| ftp-98.pdf | 253 | Intranet
| Report | Sofronie-Stokkermans, Viorica | Resolution-based Theorem Proving for SHn-Logics | 1998 |
| evaluation.ps | 171 |
| Proceedings Article | [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 | 2001 |
| entcs-pdpar06-jacobs-sofronie.pdf | 337 | Internal
| Electronic Journal Article | 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 | 2007 |
| diss.pdf | 1158 | Public
| Thesis - Doctoral dissertation | Ihlemann, Carsten | Reasoning in Combinations of Theories
Universität des Saarlandes | 2010 |
| dissertation_wischnewski.pdf | 859 | Internal
| Thesis - Doctoral dissertation | Wischnewski, Patrick | Efficient Reasoning Procedures for Complex First-Order Theories
Universität des Saarlandes | 2012 |
| diplom-2006-03-13.pdf | 2462 | Public
| Thesis - Diploma thesis | Bankstahl, Jan | Netflow analysis of SAP R/3 traffic in an enterprise environment
Universität des Saarlandes | 2006 |
| decIndQueries_TR.pdf | 390 | Public
| Report | Horbach, Matthias
Weidenbach, Christoph | Deciding the Inductive Validity of Forall Exists* Queries | 2009 |
| DDD+2010.pdf | 339 | Intranet
| Electronic Journal Article | [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 | 2011 |
| citius.ps | 357 | Public
| Electronic Proceedings Article | 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 | 2003 |
| CarstenKarl.PDF | 1101 | Intranet
| Thesis - Master's thesis | Karl, Carsten | Automatische Analyse von Layer 3 Netzwerken mit SPASS
Universität des Saarlandes | 2006 |
| cade-99.pdf | 248 | Public
| Proceedings Article | 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 | 1999 |
| BaThesis.pdf | 200 | Intranet
| Thesis - Bachelor thesis | Dimova, Dilyana | Propositional Abduction
Universität des Saarlandes | 2007 |
| ba-thesis.pdf | 493 | Internal
| Thesis - Bachelor thesis | Bromberger, Martin | Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic
Universität des Saarlandes | 2012 |
| AtomFinal.ps | 547 |
| Proceedings Article | 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 | 2001 |
| art%3A10.1007%2Fs11786-012-0135-4-1.pdf | 410 | Internal
| Journal Article | Kruglov, Evgeny
Weidenbach, Christoph | Superposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456 | 2012 |
| analysis.ps | 81 | Public
| Proceedings Article | 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 | 2002 |
| 10-1.1007_s11786-012-0135-4.pdf | 436 | Internal
| Journal Article | Kruglov, Evgeny
Weidenbach, Christoph | Superposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456 | 2012 |
