Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF RG1 Publications

MPI-INF RG1 Publications

Entries sorted by: 1. Author,Editor - 1. by Individual - 1. by Names

Login to this database


 

Viewing:

1. Author,Editor - 1. by Individual - 1. by Names
Next Page
Show entries starting with: A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
#YearAuthor(s) [non member]TitleType
1
Hide details for Abdel-Rahman, Essam O.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
Hide details for Afshordel, BijanAfshordel, Bijan
2001Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph
Attachment IconFirst-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
1999Weidenbach, 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
Hide details for Althaus, ErnstAlthaus, Ernst
2009Althaus, 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
Hide details for Areces, Carlos (ed.)Areces, Carlos (ed.)
2008Sofronie-Stokkermans, VioricaLocality 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
Hide details for Autexier, Serge (ed.)Autexier, Serge (ed.)
2006Sofronie-Stokkermans, VioricaLocal reasoning in verification
In: IJCAR'06 Workshop : VERIFY'06: Verification Workshop, 128-145
Electronic Proceedings Article
1
Hide details for Avenhaus, JürgenAvenhaus, Jürgen
2003[Avenhaus, Jürgen]
Hillenbrand, Thomas
[Löchner, Bernd]
Attachment IconOn Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233
Journal Article
1
Hide details for Aziz, Zaheer (ed.)Aziz, Zaheer (ed.)
2009Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard
Attachment IconExternal Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288
Proceedings Article
1
Hide details for Azmy, NoranAzmy, Noran
2012Azmy, NoranAttachment IconFormula Renaming with Generalizations
Universität des Saarlandes
Thesis - Masters thesis
8
Hide details for Baader, Franz (ed.)Baader, Franz (ed.)
2009UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings
Electronic Proceedings
2008Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08)Proceedings
2008Jacobs, SwenAttachment IconIncremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62
Proceedings Article
2008Sofronie-Stokkermans, VioricaLocality 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
2007Sofronie-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
2003Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe
Attachment IconSuperposition 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]
Attachment IconThe New WALDMEISTER Loop at Work
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 317-321
Proceedings Article
1994Fehrer, 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
Hide details for Bachmair, LeoBachmair, Leo
1994Bachmair, 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
1994Bachmair, 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
1992Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe
Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434
Proceedings Article
1
Hide details for Bajcsy, R. (ed.)Bajcsy, R. (ed.)
1993Weidenbach, ChristophExtending the Resolution Method with Sorts
In: Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI '93), 60-65
Proceedings Article
1
Hide details for Ball, Thomas (ed.)Ball, Thomas (ed.)
2010Sofronie-Stokkermans, VioricaAutomated 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
Hide details for Bankstahl, JanBankstahl, Jan
2006Bankstahl, JanNetflow analysis of SAP R/3 traffic in an enterprise
Universität des Saarlandes
Thesis - Masters thesis
2006Bankstahl, JanAttachment IconNetflow analysis of SAP R/3 traffic in an enterprise environment
Universität des Saarlandes
Thesis - other
1
Hide details for Barth, PeterBarth, Peter
1995Barth, Peter
[Kleine Büning, Hans]
Weidenbach, Christoph
Workshop CPL Computational Propositional Logic
In: KI-95 Activities: Workshops, Posters, Demos, 71-72
Proceedings Article
1
Hide details for Basin, David (ed.)Basin, David (ed.)
2004Ganzinger, 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
Hide details for Bastuck, AndreaBastuck, Andrea
2006Bastuck, AndreaMaschinell unterstützte Analyse eines Sicherheitsprotokolls
Universität des Saarlandes
Thesis - other
2
Hide details for Baumgartner, PeterBaumgartner, Peter
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
Hide details for Beckert, Bernhard (ed.)Beckert, Bernhard (ed.)
2005Jacobs, Swen
Waldmann, Uwe
Attachment IconComparing Instance Generation Methods for Automated Reasoning
In: Automated Reasoning with Analytic Tableaux and Related Methods : International Conference, TABLEAUX 2005, 153-168
Proceedings Article
4
Hide details for Becker, Bernd (ed.)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 systemsReport
2009Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica
Constraint Solving for InterpolationReport
2008Sofronie-Stokkermans, VioricaEfficient Hierarchical Reasoning about Functions over Numerical DomainsReport
2008Sofronie-Stokkermans, VioricaSheaves and geometric logic and applications to modular verification of complex systemsReport
1
Hide details for Bendisposto, Jens (ed.)Bendisposto, Jens (ed.)
2010Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph
Attachment IconModel Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21
Proceedings Article
1
Hide details for Beringer, Lennart (ed.)Beringer, Lennart (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
4
Hide details for Bernd, Becker (ed.)Bernd, Becker (ed.)
2011[Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
PTIME parametric verification of safety properties for reasonable linear hybrid automataReport
2010[Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica
Automatic Verification of Parametric Specifications with Complex TopologiesReport
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
On hierarchical reasoning in combinations of theoriesReport
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
System Description: H-PILoT (Version 1.9)Report
1
Hide details for Berns, Karsten (ed.)Berns, Karsten (ed.)
2008Sofronie-Stokkermans, VioricaEfficient hierarchical reasoning about functions over numerical domains
In: KI 2008: Advances in Artificial Intelligence, 135-143
Proceedings Article
1
Hide details for Bibel, Wolfgang (ed.)Bibel, Wolfgang (ed.)
1998Weidenbach, ChristophSorted Unification and Tree Automata
In: Automated Deduction - A Basis for Applications, 291-320
Part of a Book
1
Hide details for Billington, JonathanBillington, 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
Hide details for Bjorner, NikolajBjorner, 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
Hide details for Bjørner, Nikolaj (ed.)Bjørner, Nikolaj (ed.)
2012Fietzke, 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
2012Suda, Martin
Weidenbach, Christoph
Attachment IconLabelled Superposition for PLTL
In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, 391-405
Proceedings Article
2011Automated Deduction - CADE-23 : 23rd International Conference on Automated DeductionProceedings
1
Hide details for Blanchette, Jasmin ChristianBlanchette, 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
Hide details for Bonacina, Maria Paola (ed.)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
2013Sofronie-Stokkermans, VioricaHierarchical 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
2013Hillenbrand, 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
1997Waldmann, UweA 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
Hide details for Bouajjani, Ahmed (ed.)Bouajjani, Ahmed (ed.)
2009Jacobs, SwenAttachment IconIncremental Instance Generation in Local Reasoning
In: Computer Aided Verification : 21st International Conference, CAV 2009, 368-382
Proceedings Article
2
Hide details for Brahm, UweBrahm, Uwe
2002Weidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor
Attachment IconSPASS Version 2.0
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 275-279
Proceedings Article
1999Weidenbach, 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
Hide details for Breuel, Thomas (ed.)Breuel, Thomas (ed.)
2008Sofronie-Stokkermans, VioricaEfficient hierarchical reasoning about functions over numerical domains
In: KI 2008: Advances in Artificial Intelligence, 135-143
Proceedings Article
1
Hide details for Broda, Krysia (ed.)Broda, Krysia (ed.)
1994Weidenbach, ChristophFirst-Order Tableaux with Sorts
In: TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 247-261
Proceedings Article
1
Hide details for Bromberger, MartinBromberger, Martin
2012Bromberger, MartinAttachment IconAdapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic
Universität des Saarlandes
Thesis - Bachelor thesis
1
Hide details for Bruni, Roberto (ed.)Bruni, Roberto (ed.)
2011Lu, 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
Hide details for Bultan, Tevfik (ed.)Bultan, Tevfik (ed.)
2013[Dhungana, Deepak]
Tang, Ching Hoo
Weidenbach, Christoph
[Wischnewski, Patrick]
Attachment IconAutomated Verification of Interactive Rule-Based Configuration Systems
In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 551-561
Proceedings Article
2
Hide details for Burel, GuillaumeBurel, Guillaume
2011Burel, GuillaumeEfficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
In: Logical Methods in Computer Science [7], 3:1-3:31
Electronic Journal Article
2010Burel, GuillaumeEmbedding 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
Hide details for Cachro, Jacek (ed.)Cachro, Jacek (ed.)
1999Sofronie-Stokkermans, VioricaResolution-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
Hide details for Charatonik, Witold (ed.)Charatonik, Witold (ed.)
2002Hillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor
Attachment IconIs 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
Hide details for Cha, Sungdeok (Steve) (ed.)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
Hide details for Choi, Jin-Young (ed.)Choi, Jin-Young (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
Hide details for Christophe Ringeissen (ed.)Christophe Ringeissen (ed.)
2013[Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas
Attachment IconPresburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70
Proceedings Article
1
Hide details for Ciobanu, Gabriel (ed.)Ciobanu, Gabriel (ed.)
1999Sofronie-Stokkermans, Viorica
[Stokkermans, Karel]
Attachment IconModeling Interaction by Sheaves and Geometric Logic
In: Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99), 512-523
Proceedings Article
1
Hide details for Clarke, Edmund M. (ed.)Clarke, Edmund M. (ed.)
2010Horbach, MatthiasDisunification for Ultimately Periodic Interpretations
In: Logic for Programming, Artificial Intelligence, and Reasoning : 16th International Conference, LPAR-16, 290-311
Proceedings Article
2
Hide details for Cohrs, ChristianCohrs, Christian
1999Weidenbach, 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
1998Weidenbach, Christoph
Meyer, Christoph
Cohrs, Christian
Engel, Thorsten
Keen, Enno
SPASS V0.77
In: Journal of Automated Reasoning [21], 113-113
Journal Article
1
Hide details for Contejean, Evelyne (ed.)Contejean, Evelyne (ed.)
2007Sofronie-Stokkermans, VioricaOn 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
Hide details for Cook, Byron (ed.)Cook, Byron (ed.)
2007Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica
Constraint Solving for Interpolation
In: Verification, Model Checking and Abstract Interpretation : 8th International Conference, VMCAI 2007, 346-362
Proceedings Article
2007Sofronie-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
2006Jacobs, 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
Hide details for Cruz, Rene L. (ed.)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
Hide details for D'Agostino, Marcello (ed.)D'Agostino, Marcello (ed.)
1994Weidenbach, ChristophFirst-Order Tableaux with Sorts
In: TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 247-261
Proceedings Article
1
Hide details for Dahn, Ingo (ed.)Dahn, Ingo (ed.)
2003Hillenbrand, ThomasAttachment IconCitius 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
Hide details for Damm, WernerDamm, 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]
Attachment IconExact 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 systemsReport
2011[Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
PTIME parametric verification of safety properties for reasonable linear hybrid automataReport
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
Hide details for Damm, Werner Martin (ed.)Damm, Werner Martin (ed.)
2009Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica
Constraint Solving for InterpolationReport
2008Sofronie-Stokkermans, VioricaEfficient Hierarchical Reasoning about Functions over Numerical DomainsReport
2008Sofronie-Stokkermans, VioricaSheaves and geometric logic and applications to modular verification of complex systemsReport
5
Hide details for Damm, Werner (ed.)Damm, Werner (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 systemsReport
2011[Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
PTIME parametric verification of safety properties for reasonable linear hybrid automataReport
2010[Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica
Automatic Verification of Parametric Specifications with Complex TopologiesReport
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
On hierarchical reasoning in combinations of theoriesReport
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
System Description: H-PILoT (Version 1.9)Report
1
Hide details for Davies, Jim	 (ed.)Davies, Jim (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
1
Hide details for Dawar, Anuj (ed.)Dawar, Anuj (ed.)
2010Burel, GuillaumeEmbedding 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
Hide details for de Melo, Gerardde Melo, Gerard
2009Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard
Attachment IconExternal Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288
Proceedings Article
2
Hide details for de Nivelle, Hans (ed.)de Nivelle, Hans (ed.)
2006Hillenbrand, Thomas
Topic, Dalibor
Weidenbach, Christoph
Sudokus as Logical Puzzles
In: Disproving'06: Non-Theorems, Non-Validity, Non-Provability, 2-12
Proceedings Article
2001Hillenbrand, Thomas
[Löchner, Bernd]
Attachment IconThe Next WALDMEISTER Loop (Extended Abstract)
In: Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001, 13-21
Proceedings Article
1
Hide details for de Swart, Harrie (ed.)de Swart, Harrie (ed.)
1998Hustadt, 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
Hide details for Denney, Ewen (ed.)Denney, Ewen (ed.)
2013[Dhungana, Deepak]
Tang, Ching Hoo
Weidenbach, Christoph
[Wischnewski, Patrick]
Attachment IconAutomated Verification of Interactive Rule-Based Configuration Systems
In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 551-561
Proceedings Article
1
Hide details for Dershowitz, Nachum (ed.)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
Hide details for Dhungana, DeepakDhungana, Deepak
2013[Dhungana, Deepak]
Tang, Ching Hoo
Weidenbach, Christoph
[Wischnewski, Patrick]
Attachment IconAutomated Verification of Interactive Rule-Based Configuration Systems
In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 551-561
Proceedings Article
2
Hide details for Dierks, HenningDierks, 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]
Attachment IconExact 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
Hide details for Dimova, DilyanaDimova, Dilyana
2009Dimova, DilyanaOn the Translation of Timed Automata into First-order Logic
Universität des Saarlandes
Thesis - Masters thesis
2009Weidenbach, 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
2007Dimova, DilyanaAttachment IconPropositional Abduction
Universität des Saarlandes
Thesis - Bachelor thesis
1
Hide details for Dingel, Juergen (ed.)Dingel, Juergen (ed.)
2011Lu, 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
Hide details for Disch, StefanDisch, Stefan
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]
Attachment IconExact 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 systemsReport
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
Hide details for Dreschler-Fischer, Leonie (ed.)Dreschler-Fischer, Leonie (ed.)
1995Barth, Peter
[Kleine Büning, Hans]
Weidenbach, Christoph
Workshop CPL Computational Propositional Logic
In: KI-95 Activities: Workshops, Posters, Demos, 71-72
Proceedings Article
2
Hide details for Dreßler, ChristianDreßler, Christian
2009Dreßler, ChristianAttachment IconAutomatic Analysis of Tree-Based Feature Models with SPASS
Universität des Saarlandes
Thesis - Masters thesis
2007[Dressler, Christian]Attachment IconFirst-Order Proof Documentation
Universität des Saarlandes
Thesis - Bachelor thesis
1
Hide details for Eggers, AndreasEggers, Andreas
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
Hide details for Egly, Uwe (ed.)Egly, Uwe (ed.)
2002Sofronie-Stokkermans, VioricaAttachment IconOn 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
Hide details for Eiswirth, M.Eiswirth, M.
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
Hide details for Eklund, Patrick (ed.)Eklund, Patrick (ed.)
1998Sofronie-Stokkermans, VioricaRepresentation 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
Hide details for Engel, ThorstenEngel, Thorsten
1999Weidenbach, 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
1998Weidenbach, Christoph
Meyer, Christoph
Cohrs, Christian
Engel, Thorsten
Keen, Enno
SPASS V0.77
In: Journal of Automated Reasoning [21], 113-113
Journal Article
1
Hide details for Errami, H.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
Hide details for Escalada-Imaz, Gonzalo (ed.)Escalada-Imaz, Gonzalo (ed.)
1998Sofronie-Stokkermans, VioricaRepresentation 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
Hide details for Esquivel Pinto, Claudia SofiaEsquivel Pinto, Claudia So fia
2013Esquivel Pinto, Claudia So fiaAttachment IconComputing Variable Orders for SAT-Problems
Universität des Saarlandes
Thesis - Masters thesis
1
Hide details for et. al. (ed.)et. al. (ed.)
1994Weidenbach, ChristophFirst-Order Tableaux with Sorts
In: TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 247-261
Proceedings Article
3
Hide details for Faber, JohannesFaber, Johannes
2010[Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica
Automatic Verification of Parametric Specifications with Complex TopologiesReport
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
Hide details for Fehrer, DetlefFehrer, Detlef
1994Fehrer, 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
Hide details for Felty, Amy (ed.)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
Hide details for Fermüller, Christian G. (ed.)Fermüller, Christian G. (ed.)
2010Fietzke, 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
Hide details for Fermüller, Christian (ed.)Fermüller, Christian (ed.)
2002Sofronie-Stokkermans, VioricaAttachment IconOn 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
Hide details for Ferreirim, Isabel (ed.)Ferreirim, Isabel (ed.)
1999Sofronie-Stokkermans, VioricaPriestley representation for distributive lattices with operators and applications to automated theorem proving
In: Dualities, Interpretability and Ordered Structures, 43-54
Proceedings Article
1
Hide details for Fiedler, Herbert (ed.)Fiedler, Herbert (ed.)
1998Weidenbach, ChristophRechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197
Part of a Book
9
Hide details for Fietzke, ArnaudFietzke, Arnaud
2012Fietzke, 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
2012Fietzke, Arnaud
Weidenbach, Christoph
Superposition as a Decision Procedure for Timed Automata
In: Mathematics in Computer Science [6], 409-425
Electronic Journal Article
2011Fietzke, 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
2010Fietzke, 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
2009Fietzke, Arnaud
Weidenbach, Christoph
Labelled Splitting
In: Annals of Mathematics and Artificial Intelligence [55], 3-34
Journal Article
2009Weidenbach, 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
2008Fietzke, Arnaud
Weidenbach, Christoph
Attachment IconLabelled SplittingReport
2008Fietzke, Arnaud
Weidenbach, Christoph
Labelled Splitting
In: IJCAR, 459-474
Proceedings Article
2007Fietzke, ArnaudAttachment IconLabelled Splitting
Universität des Saarlandes
Thesis - Masters thesis
1
Hide details for Finkbeiner, Bernd (ed.)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 systemsReport
1
Hide details for Fitting, Melvin (ed.)Fitting, Melvin (ed.)
2003Sofronie-Stokkermans, VioricaAttachment IconRepresentation 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
Hide details for Fontaine, PascalFontaine, 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
Hide details for Fontaine, Pascal (ed.)Fontaine, Pascal (ed.)
2013Horbach, Matthias
Sofronie-Stokkermans, Viorica
Obtaining Finite Local Theory Axiomatizations via Saturation
In: Frontiers of Combining Systems - 9th International Symposium, 198-213
Proceedings Article
8
Hide details for Fränzle, Martin (ed.)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 systemsReport
2011[Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
PTIME parametric verification of safety properties for reasonable linear hybrid automataReport
2010[Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica
Automatic Verification of Parametric Specifications with Complex TopologiesReport
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
On hierarchical reasoning in combinations of theoriesReport
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
System Description: H-PILoT (Version 1.9)Report
2009Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica
Constraint Solving for InterpolationReport
2008Sofronie-Stokkermans, VioricaEfficient Hierarchical Reasoning about Functions over Numerical DomainsReport
2008Sofronie-Stokkermans, VioricaSheaves and geometric logic and applications to modular verification of complex systemsReport
1
Hide details for Frazzoli, Emilio (ed.)Frazzoli, Emilio (ed.)
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
Hide details for Freiheit, JörnFreiheit, Jörn
2007Freiheit, 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
2006Freiheit, 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
2006Freiheit, 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
Hide details for Furbach, Ulrich (ed.)Furbach, Ulrich (ed.)
2006Sofronie-Stokkermans, VioricaAttachment IconInterpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250
Proceedings Article
1997Waldmann, UweA 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
Hide details for Gaede, BerndGaede, Bernd
1996Weidenbach, 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
Hide details for Gaillourdet, Jean-MarieGaillourdet, Jean-Marie
2003[Gaillourdet, Jean-Marie]
Hillenbrand, Thomas
[Löchner, Bernd]
[Spies, Hendrik]
Attachment IconThe New WALDMEISTER Loop at Work
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 317-321
Proceedings Article
15
Hide details for Ganzinger, HaraldGanzinger, Harald
2006Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Waldmann, Uwe
Modular Proof Systems for Partial Functions with Evans Equality
In: Information and Computation [204], 1453-1492
Journal Article
2006Ganzinger, Harald
[Korovin, Konstantin]
Theory Instantiation
In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06), 497-511
Proceedings Article
2004Ganzinger, 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
2003Ganzinger, Harald
Korovin, Konstantin
Attachment IconNew Directions in Instantiation-Based Theorem Proving
In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), 55-64
Proceedings Article
2003Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe
Attachment IconSuperposition modulo a Shostak Theory
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 182-196
Proceedings Article
2000Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Attachment IconChaining 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
1997Ganzinger, 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
1996Ganzinger, 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
1994Bachmair, 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
1994Bachmair, Leo
Ganzinger, Harald
Rewrite-based equational theorem proving with selection and simplification
In: Journal of Logic and Computation [4], 217-247
Journal Article
1994Ganzinger, HaraldThe Saturate SystemUnpublished/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
1992Ganzinger, 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
1992Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe
Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434
Proceedings Article
5
Hide details for Ganzinger, Harald (ed.)Ganzinger, Harald (ed.)
2002Hillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor
Attachment IconIs 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
1999Waldmann, UweCancellative 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
1999Sofronie-Stokkermans, VioricaAttachment IconOn 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
1999Weidenbach, 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
1999Weidenbach, ChristophTowards 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
Hide details for Gasse, FrancisGasse, Francis
2011Gasse, 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
Hide details for Ghilardi, SilvioGhilardi, 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
Hide details for Ghilardi, Silvio (ed.)Ghilardi, Silvio (ed.)
2009Althaus, 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
2009UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings
Electronic Proceedings
2008Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08)Proceedings
2008Jacobs, SwenAttachment IconIncremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62
Proceedings Article
2007Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07)Proceedings
1
Hide details for Gibbons, Jeremy (ed.)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
Hide details for Giesl, Jürgen (ed.)Giesl, Jürgen (ed.)
2010Sofronie-Stokkermans, VioricaAutomated 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
2010Sofronie-Stokkermans, VioricaHierarchical Reasoning for the Verification of Parametric Systems
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 171-187
Proceedings Article
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
On Hierarchical Reasoning in Combinations of Theories
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 30-45
Proceedings Article
2010Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick
On the Saturation of YAGO
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 441-456
Proceedings Article
2007Sofronie-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
Hide details for Goldblatt, Robert (ed.)Goldblatt, Robert (ed.)
2008Sofronie-Stokkermans, VioricaLocality 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
Hide details for Goré, Rajeev (ed.)Goré, Rajeev (ed.)
2001[Nieuwenhuis, Robert]
Hillenbrand, Thomas
[Riazanov, Alexandre]
[Voronkov, Andrei]
Attachment IconOn the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271
Proceedings Article
2001Waldmann, UweSuperposition and Chaining for Totally Ordered Divisible Abelian Groups (Extended Abstract)
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 226-241
Proceedings Article
1
Hide details for Gorny, Peter (ed.)Gorny, Peter (ed.)
1998Weidenbach, ChristophRechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197
Part of a Book
1
Hide details for Gottlob, Georg (ed.)Gottlob, Georg (ed.)
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
Hide details for Grädel, Erich (ed.)Grädel, Erich (ed.)
2009Horbach, 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
Hide details for Graf, Susanne (ed.)Graf, Susanne (ed.)
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
Hide details for Gramlich, Bernhard (ed.)Gramlich, Bernhard (ed.)
2012Suda, Martin
Weidenbach, Christoph
Attachment IconA PLTL-prover based on labelled superposition with partial model guidance
In: Automated Reasoning : 6th International Joint Conference, IJCAR 2012, 537-543
Proceedings Article
1
Hide details for Grass, Werner (ed.)Grass, Werner (ed.)
1998Weidenbach, ChristophRechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197
Part of a Book
1
Hide details for Grigoriev. D.Grigoriev. D.
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
Hide details for Grosu, Radu (ed.)Grosu, Radu (ed.)
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
Hide details for Hähnle, ReinerHähnle, Reiner
1996[Hähnle, Reiner]
[Kerber, Manfred]
Weidenbach, Christoph
Common Syntax of the DFG-Schwerpunktprogramm ``Deduktion''Report
5
Hide details for Hähnle, Reiner (ed.)Hähnle, Reiner (ed.)
2010Sofronie-Stokkermans, VioricaAutomated 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
2010Sofronie-Stokkermans, VioricaHierarchical Reasoning for the Verification of Parametric Systems
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 171-187
Proceedings Article
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
On Hierarchical Reasoning in Combinations of Theories
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 30-45
Proceedings Article
2010Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick
On the Saturation of YAGO
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 441-456
Proceedings Article
1998Sofronie-Stokkermans, VioricaRepresentation 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
Hide details for Hagemann, WillemHagemann, Willem
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]
Attachment IconExact 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 systemsReport
1
Hide details for Hermanns, HolgerHermanns, Holger
2010Fietzke, 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
Hide details for Hermann, Miki (ed.)Hermann, Miki (ed.)
2009UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings
Electronic Proceedings
2008Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08)Proceedings
2008Jacobs, SwenAttachment IconIncremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62
Proceedings Article
2006Ganzinger, Harald
[Korovin, Konstantin]
Theory Instantiation
In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06), 497-511
Proceedings Article
1996Weidenbach, ChristophSorted 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
Hide details for Higashino, Teruo (ed.)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
Hide details for Hillenbrand, ThomasHillenbrand, Thomas
2013Hillenbrand, 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
2013Hillenbrand, 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
2008Hillenbrand, ThomasAttachment IconSuperposition and Decision Procedures -- Back and Forth
Universität des Saarlandes
Thesis - PhD thesis
2007Hillenbrand, Thomas
Weidenbach, Christoph
Attachment IconSuperposition for Finite DomainsReport
2007Weidenbach, Christoph
[Schmidt, Renate]
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor
Attachment IconSystem Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520
Proceedings Article
2006Hillenbrand, Thomas
Topic, Dalibor
Weidenbach, Christoph
Sudokus as Logical Puzzles
In: Disproving'06: Non-Theorems, Non-Validity, Non-Provability, 2-12
Proceedings Article
2004Hillenbrand, ThomasAttachment IconA 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
2003Hillenbrand, ThomasAttachment IconCitius 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]
Attachment IconOn Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233
Journal Article
2003Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe
Attachment IconSuperposition 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]
Attachment IconThe 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
Attachment IconA Phytography of WALDMEISTER
In: AI Communications [15], 127-133
Journal Article
2002Hillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor
Attachment IconIs 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
2002Weidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor
Attachment IconSPASS Version 2.0
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 275-279
Proceedings Article
2002Hillenbrand, Thomas
[Löchner, Bernd]
Attachment IconThe Next WALDMEISTER Loop
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 486-500
Proceedings Article
2001Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph
Attachment IconFirst-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]
Attachment IconOn the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271
Proceedings Article
2001Hillenbrand, Thomas
[Löchner, Bernd]
Attachment IconThe Next WALDMEISTER Loop (Extended Abstract)
In: Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001, 13-21
Proceedings Article
2
Hide details for Hirth, SimonHirth, Simon
2007Hirth, Simon
Karl, Carsten
Weidenbach, Christoph
Attachment IconAutomatic Analysis of LAN InfrastructuresReport
2006Hirth, SimonAttachment IconAutomatische Analyse von DHCP und höheren Infrasturkturdiensten mit SPASS
Universität des Saarlandes
Thesis - Masters thesis
1
Hide details for Hölldobler, Steffen (ed.)Hölldobler, Steffen (ed.)
1998Weidenbach, ChristophRechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197
Part of a Book
11
Hide details for Horbach, MatthiasHorbach, 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
2013Horbach, MatthiasINFORMATIK 2013 - Informatik angepasst an Mensch, Organisation und UmweltBook
2013Horbach, Matthias
Sofronie-Stokkermans, Viorica
Obtaining Finite Local Theory Axiomatizations via Saturation
In: Frontiers of Combining Systems - 9th International Symposium, 198-213
Proceedings Article
2010Horbach, MatthiasDisunification for Ultimately Periodic Interpretations
In: Logic for Programming, Artificial Intelligence, and Reasoning : 16th International Conference, LPAR-16, 290-311
Proceedings Article
2010Horbach, MatthiasSuperposition-based Decision Procedures for Fixed Domain and Minimal Model Semantics
Universität des Saarlandes
Thesis - PhD thesis
2010Horbach, Matthias
Weidenbach, Christoph
Superposition for Fixed Domains
In: ACM Transactions on Computational Logic [11], 27,1-27,35
Journal Article
2009Horbach, 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
2009Horbach, 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
2009Horbach, Matthias
Weidenbach, Christoph
Attachment IconDeciding the Inductive Validity of Forall Exists* QueriesReport
2009Horbach, Matthias
Weidenbach, Christoph
Attachment IconSuperposition for Fixed DomainsReport
2008Horbach, Matthias
Weidenbach, Christoph
Superposition for Fixed Domains
In: CSL, 293-307
Proceedings Article
1
Hide details for Horbach, Matthias (ed.)Horbach, Matthias (ed.)
2013Horbach, MatthiasINFORMATIK 2013 - Informatik angepasst an Mensch, Organisation und UmweltBook
1
Hide details for Hotz, Günter (ed.)Hotz, Günter (ed.)
1998Weidenbach, ChristophRechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197
Part of a Book
1
Hide details for Hund, Marcus (ed.)Hund, Marcus (ed.)
2009Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard
Attachment IconExternal Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288
Proceedings Article
2
Hide details for Hungar, HardiHungar, 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
Hide details for Hustadt, UllrichHustadt, Ullrich
1998Hustadt, 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
1994Fehrer, 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
Hide details for Ihlemann, CarstenIhlemann, 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 automataReport
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 TopologiesReport
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
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
On hierarchical reasoning in combinations of theoriesReport
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
On Hierarchical Reasoning in Combinations of Theories
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 30-45
Proceedings Article
2010Ihlemann, CarstenAttachment IconReasoning in Combinations of Theories
Universität des Saarlandes
Thesis - PhD thesis
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
System Description: H-PILoT (Version 1.9)Report
2009Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
System Description: H-PILoT
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 131-139
Proceedings Article
2008Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica
On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281
Proceedings Article
2007Sofronie-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
2007Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Automated reasoning in some local extensions of ordered structures
In: Proceedings of ISMVL 2007, Article1
Proceedings Article
2007Sofronie-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
Hide details for Iorgulescu, Afrodita (ed.)Iorgulescu, Afrodita (ed.)
2007Sofronie-Stokkermans, VioricaAlgebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493
Part of a Book
1
Hide details for Iturrioz, LuisaIturrioz, Luisa
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
Hide details for Iturrioz, Luisa (ed.)Iturrioz, Luisa (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
2000Sofronie-Stokkermans, VioricaSome 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
Hide details for Jacobs, SwenJacobs, Swen
2010[Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica
Automatic Verification of Parametric Specifications with Complex TopologiesReport
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
2010Jacobs, SwenHierarchic Decision Procedures for Verification
Universität des Saarlandes
Thesis - PhD thesis
2009Jacobs, SwenAttachment IconIncremental Instance Generation in Local Reasoning
In: Computer Aided Verification : 21st International Conference, CAV 2009, 368-382
Proceedings Article
2008Jacobs, SwenAttachment IconIncremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62
Proceedings Article
2008Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica
On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281
Proceedings Article
2007Jacobs, Swen
Sofronie-Stokkermans, Viorica
Attachment IconApplications of hierarchical reasoning in the verification of complex systems
In: Electronic Notes in Theoretical Computer Science [174], 39-54
Electronic Journal Article
2007Jacobs, Swen
Waldmann, Uwe
Attachment IconComparing 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
2007Sofronie-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
2006Jacobs, 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
2006Jacobs, Swen
Waldmann, Uwe
Attachment IconComparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78
Electronic Journal Article
2005Jacobs, Swen
Waldmann, Uwe
Attachment IconComparing Instance Generation Methods for Automated Reasoning
In: Automated Reasoning with Analytic Tableaux and Related Methods : International Conference, TABLEAUX 2005, 153-168
Proceedings Article
1
Hide details for Jacquemard, FlorentJacquemard, Florent
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
Hide details for Jaeger, ManfredJaeger, Manfred
1994Fehrer, 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
Hide details for Kahle, Reinhard (ed.)Kahle, Reinhard (ed.)
2009Horbach, 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
Hide details for Kapur, DeepakKapur, Deepak
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
Hide details for Karl, CarstenKarl, Carsten
2007Hirth, Simon
Karl, Carsten
Weidenbach, Christoph
Attachment IconAutomatic Analysis of LAN InfrastructuresReport
2006Karl, CarstenAttachment IconAutomatische Analyse von Layer 3 Netzwerken mit SPASS
Universität des Saarlandes
Thesis - Masters thesis
1
Hide details for Karrenberg, RalfKarrenberg, Ralf
2013[Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas
Attachment IconPresburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70
Proceedings Article
3
Hide details for Keen, EnnoKeen, Enno
2002Weidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor
Attachment IconSPASS Version 2.0
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 275-279
Proceedings Article
1999Weidenbach, 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
1998Weidenbach, Christoph
Meyer, Christoph
Cohrs, Christian
Engel, Thorsten
Keen, Enno
SPASS V0.77
In: Journal of Automated Reasoning [21], 113-113
Journal Article
1
Hide details for Kepser, Stephan (ed.)Kepser, Stephan (ed.)
1996Weidenbach, ChristophUnification in Sort Theories
In: Proceedings of the 10th International Workshop on Unification, UNIF'96, 16-25
Proceedings Article
1
Hide details for Kerber, ManfredKerber, Manfred
1996[Hähnle, Reiner]
[Kerber, Manfred]
Weidenbach, Christoph
Common Syntax of the DFG-Schwerpunktprogramm ``Deduktion''Report
1
Hide details for Kerner, I. O. (ed.)Kerner, I. O. (ed.)
1998Weidenbach, ChristophRechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197
Part of a Book
1
Hide details for Kijania-Placek, Katarzyna (ed.)Kijania-Placek, Katarzyna (ed.)
1999Sofronie-Stokkermans, VioricaResolution-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
Hide details for Kim Moonzoo (ed.)Kim Moonzoo (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
2
Hide details for Kirchner, Claude (ed.)Kirchner, Claude (ed.)
1998Nonnengart, 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
1998Waldmann, UweSuperposition for Divisible Torsion-Free Abelian Groups
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 144-159
Proceedings Article
1
Hide details for Kirchner, HeleneKirchner, Helene
2009Tran, 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
Hide details for Kirchner, Hélène (ed.)Kirchner, Hélène (ed.)
1998Nonnengart, 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
1998Waldmann, UweSuperposition for Divisible Torsion-Free Abelian Groups
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 144-159
Proceedings Article
1992Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe
Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434
Proceedings Article
1
Hide details for Kleine Büning, HansKleine Büning, Hans
1995Barth, Peter
[Kleine Büning, Hans]
Weidenbach, Christoph
Workshop CPL Computational Propositional Logic
In: KI-95 Activities: Workshops, Posters, Demos, 71-72
Proceedings Article
1
Hide details for Kolaitis, Phokion (ed.)Kolaitis, Phokion (ed.)
2003Ganzinger, Harald
Korovin, Konstantin
Attachment IconNew Directions in Instantiation-Based Theorem Proving
In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), 55-64
Proceedings Article
1
Hide details for Konev, Boris (ed.)Konev, Boris (ed.)
2007Sofronie-Stokkermans, VioricaHierarchical 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
Hide details for Korovin, KonstantinKorovin, Konstantin
2006Ganzinger, Harald
[Korovin, Konstantin]
Theory Instantiation
In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06), 497-511
Proceedings Article
2003Ganzinger, Harald
Korovin, Konstantin
Attachment IconNew Directions in Instantiation-Based Theorem Proving
In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), 55-64
Proceedings Article
2
Hide details for Košta, MarekKošta, Marek
2013[Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas
Attachment IconPresburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70
Proceedings Article
2013Košta, MarekSMT-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
Hide details for Košta, Marek (ed.)Košta, Marek (ed.)
2013Košta, MarekSMT-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
Hide details for Kruglov, EvgenyKruglov, Evgeny
2013Kruglov, EvgenyAttachment IconSuperposition Modulo Theory
Universität des Saarlandes
Thesis - PhD thesis
2012Fietzke, 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
2012Kruglov, Evgeny
Weidenbach, Christoph
Attachment IconSuperposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456
Journal Article
2012Kruglov, Evgeny
Weidenbach, Christoph
Attachment IconSuperposition 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
2011Kruglov, 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
2009Althaus, 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
2008Kruglov, EvgenySuperposition Modulo Linear Arithmetic
Universität des Saarlandes
Thesis - Masters thesis
1
Hide details for Kunze, Jürgen (ed.)Kunze, Jürgen (ed.)
1994Weidenbach, ChristophSorts, Resolution, Tableaux and Propositional Logic
In: KI-94 Workshops: Extended Abstracts, 315-316
Proceedings Article
1
Hide details for Kupferschmid, StefanKupferschmid, Stefan
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
Hide details for Lamotte-Schubert, ManuelLamotte-Schubert, Manuel
2009Lamotte-Schubert, Manuel
Weidenbach, Christoph
Attachment IconAnalysis 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
2009Lamotte-Schubert, Manuel
Weidenbach, Christoph
Analysis of Authorizations in SAP R/3
In: FTP 2009 : First-Order Theorem Proving, 90-104
Electronic Proceedings Article
2009Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard
Attachment IconExternal Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288
Proceedings Article
1
Hide details for Lamotte, ManuelLamotte, Manuel
2008Lamotte, ManuelAttachment IconAnalysis of Authorizations in SAP R/3
Fachhochschule Trier
Thesis - Masters thesis
1
Hide details for Lasaruk, AlessLasaruk, Aless
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
Hide details for Lee, Insup (ed.)Lee, Insup (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
3
Hide details for Leitsch, Alexander (ed.)Leitsch, Alexander (ed.)
2001[Nieuwenhuis, Robert]
Hillenbrand, Thomas
[Riazanov, Alexandre]
[Voronkov, Andrei]
Attachment IconOn the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271
Proceedings Article
2001Waldmann, UweSuperposition 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
Hide details for Lenzerini, Maurizio (ed.)Lenzerini, Maurizio (ed.)
1994Fehrer, 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
Hide details for Lenzini, Luciano (ed.)Lenzini, Luciano (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
Hide details for Letz, ReinholdLetz, Reinhold
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
Hide details for Leuschel, Michael (ed.)Leuschel, Michael (ed.)
2010Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph
Attachment IconModel Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21
Proceedings Article
1
Hide details for Lev-Ami, TalLev-Ami, Tal
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
Hide details for Levi, G. (ed.)Levi, G. (ed.)
1992Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe
Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434
Proceedings Article
1
Hide details for Leykin, Anton (ed.)Leykin, Anton (ed.)
2011Sturm, 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
Hide details for Lilith, NimrodLilith, Nimrod
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
Hide details for Löchner, BerndLöchner, Bernd
2003[Avenhaus, Jürgen]
Hillenbrand, Thomas
[Löchner, Bernd]
Attachment IconOn 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]
Attachment IconThe 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
Attachment IconA Phytography of WALDMEISTER
In: AI Communications [15], 127-133
Journal Article
2002Hillenbrand, Thomas
[Löchner, Bernd]
Attachment IconThe Next WALDMEISTER Loop
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 486-500
Proceedings Article
2001Hillenbrand, Thomas
[Löchner, Bernd]
Attachment IconThe Next WALDMEISTER Loop (Extended Abstract)
In: Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001, 13-21
Proceedings Article
2
Hide details for Ludwig, MichelLudwig, Michel
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
2006Ludwig, MichelExtensions of the Knuth-Bendix Ordering with LPO-like Properties
Universität des Saarlandes
Thesis - Masters thesis
1
Hide details for Lutz, Carsten (ed.)Lutz, Carsten (ed.)
2008Sofronie-Stokkermans, VioricaLocality 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
Hide details for Luuk, MarcLuuk, Marc
2006Freiheit, 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
Hide details for Lu, QiLu, 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
Hide details for Lu, TianxiangLu, Tianxiang
2013Lu, TianxiangAttachment IconFormal Verification of the Pastry Protocol
Universität des Saarlandes
Thesis - PhD thesis
2011Lu, 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
2010Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph
Attachment IconModel Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21
Proceedings Article
1
Hide details for Lynch, ChristopherLynch, 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
Hide details for Lynch, Christopher (ed.)Lynch, Christopher (ed.)
2009UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings
Electronic Proceedings
1
Hide details for Maler, Oded (ed.)Maler, Oded (ed.)
2009Jacobs, SwenAttachment IconIncremental Instance Generation in Local Reasoning
In: Computer Aided Verification : 21st International Conference, CAV 2009, 368-382
Proceedings Article
1
Hide details for Mantel, Heiko (ed.)Mantel, Heiko (ed.)
2006Sofronie-Stokkermans, VioricaLocal reasoning in verification
In: IJCAR'06 Workshop : VERIFY'06: Verification Workshop, 128-145
Electronic Proceedings Article
1
Hide details for Marcus, Solomon (ed.)Marcus, Solomon (ed.)
2007Sofronie-Stokkermans, VioricaAlgebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493
Part of a Book
2
Hide details for Matheis, ThomasMatheis, 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
Hide details for McAllester, David (ed.)McAllester, David (ed.)
2000Sofronie-Stokkermans, VioricaAttachment IconOn unification for bounded distributive lattices
In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), 465-481
Proceedings Article
1999Waldmann, UweCancellative 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
Hide details for McCune, William (ed.)McCune, William (ed.)
1997Ganzinger, 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
Hide details for McRobbie, Michael A. (ed.)McRobbie, Michael A. (ed.)
1996Ganzinger, 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
Hide details for McRobbie, M. A. (ed.)McRobbie, M. A. (ed.)
1996Weidenbach, 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
1996Weidenbach, ChristophUnification in Pseudo-Linear Sort Theories is Decidable
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 343-357
Proceedings Article
1
Hide details for Mendling, Jan (ed.)Mendling, Jan (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
1
Hide details for Mertsching, Bärbel (ed.)Mertsching, Bärbel (ed.)
2009Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard
Attachment IconExternal Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288
Proceedings Article
1
Hide details for Mery, Dominique (ed.)Mery, Dominique (ed.)
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
Hide details for Merz, StephanMerz, Stephan
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
2011Lu, 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
2010Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph
Attachment IconModel Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21
Proceedings Article
1
Hide details for Merz, Stephan (ed.)Merz, Stephan (ed.)
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
Hide details for Meyer, ChristophMeyer, Christoph
1998Weidenbach, 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
1997Ganzinger, 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
Hide details for Miller, Dale (ed.)Miller, Dale (ed.)
2012Suda, Martin
Weidenbach, Christoph
Attachment IconA PLTL-prover based on labelled superposition with partial model guidance
In: Automated Reasoning : 6th International Joint Conference, IJCAR 2012, 537-543
Proceedings Article
1
Hide details for Motik, Boris (ed.)Motik, Boris (ed.)
2008Sofronie-Stokkermans, VioricaLocality 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
Hide details for Münch, SusanneMünch, Susanne
2006Freiheit, 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
Hide details for Mundici, Daniele (ed.)Mundici, Daniele (ed.)
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
Hide details for Nadif, Mohamed (ed.)Nadif, Mohamed (ed.)
2003Sofronie-Stokkermans, VioricaAttachment IconAutomated 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
Hide details for Namjoshi, Kedar S. (ed.)Namjoshi, Kedar S. (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
Hide details for Napoli, Amedeo (ed.)Napoli, Amedeo (ed.)
2003Sofronie-Stokkermans, VioricaAttachment IconAutomated 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
Hide details for Narendran, Paliath (ed.)Narendran, Paliath (ed.)
2009UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings
Electronic Proceedings
1
Hide details for Neumann, Stephan RouvenNeumann, Stephan Rouven
2009Neumann, Stephan RouvenAutomated Proof Generation of Possibiltiy Properties in Inductive Protocol Verification
Universität des Saarlandes
Thesis - Bachelor thesis
1
Hide details for Nguyen, ThanhVuNguyen, ThanhVu
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
Hide details for Nieuwenhuis, RobertNieuwenhuis, Robert
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]
Attachment IconOn the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271
Proceedings Article
3
Hide details for Nieuwenhuis, Robert (ed.)Nieuwenhuis, Robert (ed.)
2007Sofronie-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
2005Sofronie-Stokkermans, VioricaAttachment IconHierarchic reasoning in local theory extensions
In: Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 219-234
Proceedings Article
2001Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph
Attachment IconFirst-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
Hide details for Nipkow, Tobias (ed.)Nipkow, Tobias (ed.)
2010Sofronie-Stokkermans, VioricaAutomated 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]
Attachment IconOn the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271
Proceedings Article
2001Waldmann, UweSuperposition 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
Hide details for Nonnengart, AndreasNonnengart, Andreas
2001Nonnengart, Andreas
Weidenbach, Christoph
Computing small clause normal forms
In: Handbook of Automated Reasoning, 335-367
Part of a Book
1998Nonnengart, 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
1994Fehrer, 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
Hide details for Nüttgens, Markus (ed.)Nüttgens, Markus (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
1
Hide details for Nutt, Werner (ed.)Nutt, Werner (ed.)
1994Fehrer, 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
Hide details for Ohlbach, Hans JürgenOhlbach, Hans Jürgen
1995Ohlbach, Hans Jürgen
Weidenbach, Christoph
A Note on Assumptions about Skolem Functions
In: Journal of Automated Reasoning [15], 267-275
Journal Article
1994Fehrer, 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
Hide details for Ohlbach, Hans Jürgen (ed.)Ohlbach, Hans Jürgen (ed.)
1993Weidenbach, ChristophA New Sorted Logic
In: GWAI-92: Advances in Artificial Inteligence, Proceedings 16th German Workshop on Artificial Intelligence, 43-54
Proceedings Article
1
Hide details for Okamura, Yoshio (ed.)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
Hide details for Olbrich, SebastianOlbrich, 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
Hide details for Olderog, Ernst-Rüdiger (ed.)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 systemsReport
2011[Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
PTIME parametric verification of safety properties for reasonable linear hybrid automataReport
2010[Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica
Automatic Verification of Parametric Specifications with Complex TopologiesReport
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
On hierarchical reasoning in combinations of theoriesReport
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
System Description: H-PILoT (Version 1.9)Report
2009Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica
Constraint Solving for InterpolationReport
2008Sofronie-Stokkermans, VioricaEfficient Hierarchical Reasoning about Functions over Numerical DomainsReport
2008Sofronie-Stokkermans, VioricaSheaves and geometric logic and applications to modular verification of complex systemsReport
3
Hide details for Orlowska, Ewa (ed.)Orlowska, Ewa (ed.)
2003Sofronie-Stokkermans, VioricaAttachment IconRepresentation 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
2000Sofronie-Stokkermans, VioricaSome 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
Hide details for Pang, JunPang, Jun
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
Hide details for Pascal Fontaine (ed.)Pascal Fontaine (ed.)
2013[Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas
Attachment IconPresburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70
Proceedings Article
1
Hide details for Patel-Schneider, Peter F. (ed.)Patel-Schneider, Peter F. (ed.)
1994Fehrer, 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
Hide details for Paun, Gheorghe (ed.)Paun, Gheorghe (ed.)
1999Sofronie-Stokkermans, Viorica
[Stokkermans, Karel]
Attachment IconModeling Interaction by Sheaves and Geometric Logic
In: Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99), 512-523
Proceedings Article
1
Hide details for Peltier, NicolasPeltier, Nicolas
2012[Peltier, Nicolas]
Sofronie-Stokkermans, Viorica
First-order theorem proving: Foreword
In: Journal of Symbolic Computation [47], 1009-1010
Journal Article
5
Hide details for Peltier, Nicolas (ed.)Peltier, Nicolas (ed.)
2010First-Order Theorem Proving : Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09)Electronic Proceedings
2009Lamotte-Schubert, Manuel
Weidenbach, Christoph
Attachment IconAnalysis 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
2009Lamotte-Schubert, Manuel
Weidenbach, Christoph
Analysis of Authorizations in SAP R/3
In: FTP 2009 : First-Order Theorem Proving, 90-104
Electronic Proceedings Article
2009First-Order Theorem Proving 2009Proceedings
2009First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving, ProceedingsProceedings
1
Hide details for Pfenning, Frank (ed.)Pfenning, Frank (ed.)
2007Weidenbach, Christoph
[Schmidt, Renate]
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor
Attachment IconSystem Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520
Proceedings Article
4
Hide details for Pigorsch, FlorianPigorsch, 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]
Attachment IconExact 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
Hide details for Piskac, RuzicaPiskac, Ruzica
2013Hillenbrand, 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
Hide details for Podelski, AndreasPodelski, Andreas
2002Hillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor
Attachment IconIs 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
Hide details for Podelski, Andreas (ed.)Podelski, Andreas (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 systemsReport
2011[Damm, Werner]
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
PTIME parametric verification of safety properties for reasonable linear hybrid automataReport
2010[Faber, Johannes]
Ihlemann, Carsten
[Jacobs, Swen]
Sofronie-Stokkermans, Viorica
Automatic Verification of Parametric Specifications with Complex TopologiesReport
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
On hierarchical reasoning in combinations of theoriesReport
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
System Description: H-PILoT (Version 1.9)Report
2009Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica
Constraint Solving for InterpolationReport
2008Sofronie-Stokkermans, VioricaEfficient Hierarchical Reasoning about Functions over Numerical DomainsReport
2008Sofronie-Stokkermans, VioricaSheaves and geometric logic and applications to modular verification of complex systemsReport
2007Rybalchenko, 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
Hide details for Popescu, AndreiPopescu, Andrei
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
Hide details for Prade, Henri (ed.)Prade, Henri (ed.)
1998Sofronie-Stokkermans, VioricaOn 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
Hide details for Prevosto, VirgilePrevosto, Virgile
2006[Prevosto, Virgile]
Waldmann, Uwe
SPASS+T
In: ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 18-33
Proceedings Article
1
Hide details for Pribbenow, Simone (ed.)Pribbenow, Simone (ed.)
1995Barth, Peter
[Kleine Büning, Hans]
Weidenbach, Christoph
Workshop CPL Computational Propositional Logic
In: KI-95 Activities: Workshops, Posters, Demos, 71-72
Proceedings Article
1
Hide details for Ramakrishnan, C. R. (ed.)Ramakrishnan, C. R. (ed.)
2008Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica
On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281
Proceedings Article
1
Hide details for Ranise, SilvioRanise, Silvio
2009Tran, 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
Hide details for Ranise, Silvio (ed.)Ranise, Silvio (ed.)
2007Sofronie-Stokkermans, VioricaHierarchical 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
Hide details for Ratschan, Stefan (ed.)Ratschan, Stefan (ed.)
2011Fietzke, 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
2011Kruglov, 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
Hide details for Rehof, Jakob (ed.)Rehof, Jakob (ed.)
2008Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica
On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281
Proceedings Article
1
Hide details for Reischuk, Rüdiger (ed.)Reischuk, Rüdiger (ed.)
1998Weidenbach, ChristophRechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197
Part of a Book
1
Hide details for Remenyi, Dan (ed.)Remenyi, Dan (ed.)
2006Freiheit, Jörn
[Zangl, Fabrice]
Model-based user-interface management for public services
In: 6th European Conference on e-Government, 141-151
Proceedings Article
1
Hide details for Rémy, J.-L. (ed.)Rémy, J.-L. (ed.)
1992Ganzinger, 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
Hide details for Renate A. Schmidt (ed.)Renate A. Schmidt (ed.)
2013[Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas
Attachment IconPresburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70
Proceedings Article
1
Hide details for Reps, ThomasReps, 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
Hide details for Reuter, JochenReuter, Jochen
2013Reuter, JochenAttachment IconReal Linear Quantifier Elimination
Universität des Saarlandes
Thesis - Masters thesis
1
Hide details for Riazanov, AlexandreRiazanov, Alexandre
2001[Nieuwenhuis, Robert]
Hillenbrand, Thomas
[Riazanov, Alexandre]
[Voronkov, Andrei]
Attachment IconOn the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271
Proceedings Article
1
Hide details for Ringeissen, Christophe (ed.)Ringeissen, Christophe (ed.)
2013Horbach, Matthias
Sofronie-Stokkermans, Viorica
Obtaining Finite Local Theory Axiomatizations via Saturation
In: Frontiers of Combining Systems - 9th International Symposium, 198-213
Proceedings Article
1
Hide details for Ringeissen, ChristopherRingeissen, Christopher
2009Tran, 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
Hide details for Robinson, Alan (ed.)Robinson, Alan (ed.)
2001Weidenbach, ChristophCombining Superposition, Sorts and Splitting
In: Handbook of Automated Reasoning, 1965-2013
Part of a Book
2001Nonnengart, Andreas
Weidenbach, Christoph
Computing small clause normal forms
In: Handbook of Automated Reasoning, 335-367
Part of a Book
2
Hide details for Rock, GeorgRock, Georg
1998Nonnengart, 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
1996Weidenbach, 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
Hide details for Roggenbach, Markus (ed.)Roggenbach, Markus (ed.)
2010Lu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph
Attachment IconModel Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21
Proceedings Article
1
Hide details for Rosati, Riccardo (ed.)Rosati, Riccardo (ed.)
2011Gasse, 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
Hide details for Rudeanu, Sergiu (ed.)Rudeanu, Sergiu (ed.)
2007Sofronie-Stokkermans, VioricaAlgebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493
Part of a Book
1
Hide details for Rudolph, Sebastian (ed.)Rudolph, Sebastian (ed.)
2011Gasse, 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
Hide details for Rump, Frank J. (ed.)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
Hide details for Rusev, RostislavRusev, Rostislav
2008Rusev, RostislavAttachment IconBitvector Reasoning with SPASS
Universität des Saarlandes
Thesis - Masters thesis
2007Weidenbach, Christoph
[Schmidt, Renate]
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor
Attachment IconSystem Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520
Proceedings Article
1
Hide details for Rusinowitch, Michael (ed.)Rusinowitch, Michael (ed.)
2004Ganzinger, 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
Hide details for Rusinowitch, M. (ed.)Rusinowitch, M. (ed.)
1992Ganzinger, 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
Hide details for Rybalchenko, AndreyRybalchenko, Andrey
2010[Rybalchenko, Andrey]
Sofronie-Stokkermans, Viorica
Constraint Solving for Interpolation
In: Journal of Symbolic Computation [45], 1212-1233
Journal Article
2009Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica
Constraint Solving for InterpolationReport
2007Rybalchenko, 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
Hide details for Sagiv, MoolySagiv, Mooly
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
Hide details for Salzer, Gernot (ed.)Salzer, Gernot (ed.)
1996Weidenbach, ChristophSorted 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
Hide details for SanJuan, Eric (ed.)SanJuan, Eric (ed.)
2003Sofronie-Stokkermans, VioricaAttachment IconAutomated 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
Hide details for Sattler, Uli (ed.)Sattler, Uli (ed.)
2012Suda, Martin
Weidenbach, Christoph
Attachment IconA PLTL-prover based on labelled superposition with partial model guidance
In: Automated Reasoning : 6th International Joint Conference, IJCAR 2012, 537-543
Proceedings Article
1
Hide details for Sattler, UlrikeSattler, Ulrike
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
Hide details for Sattler, Ulrike (ed.)Sattler, Ulrike (ed.)
2008Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08)Proceedings
2008Jacobs, SwenAttachment IconIncremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62
Proceedings Article
2007Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07)Proceedings
2004Hillenbrand, ThomasAttachment IconA 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
Hide details for Scheibler, KarstenScheibler, 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
Hide details for Schmidt, RenateSchmidt, Renate
2007Weidenbach, Christoph
[Schmidt, Renate]
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor
Attachment IconSystem Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520
Proceedings Article
2
Hide details for Schmidt, Renate A.Schmidt, Renate A.
1998Hustadt, 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
1994Fehrer, 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
Hide details for Schmidt, Renate A. (ed.)Schmidt, Renate A. (ed.)
2013Horbach, Matthias
Sofronie-Stokkermans, Viorica
Obtaining Finite Local Theory Axiomatizations via Saturation
In: Frontiers of Combining Systems - 9th International Symposium, 198-213
Proceedings Article
2009Horbach, 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
2009Sofronie-Stokkermans, VioricaLocality results for certain extensions of theories with bridging functions
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 67-83
Proceedings Article
2009Weidenbach, 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
2009Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
System Description: H-PILoT
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 131-139
Proceedings Article
1
Hide details for Schmidt, Renate (ed.)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
Hide details for Schmitt, Peter H. (ed.)Schmitt, Peter H. (ed.)
1998Weidenbach, ChristophSorted Unification and Tree Automata
In: Automated Deduction - A Basis for Applications, 291-320
Part of a Book
5
Hide details for Scholl, ChristophScholl, 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]
Attachment IconExact 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 systemsReport
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
Hide details for Schulz, Klaus U. (ed.)Schulz, Klaus U. (ed.)
1996Weidenbach, ChristophUnification in Sort Theories
In: Proceedings of the 10th International Workshop on Unification, UNIF'96, 16-25
Proceedings Article
2
Hide details for Schulz, Stephan (ed.)Schulz, Stephan (ed.)
2006[Prevosto, Virgile]
Waldmann, Uwe
SPASS+T
In: ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 18-33
Proceedings Article
2001Hillenbrand, Thomas
[Löchner, Bernd]
Attachment IconThe Next WALDMEISTER Loop (Extended Abstract)
In: Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001, 13-21
Proceedings Article
2
Hide details for Sebastiani, Roberto (ed.)Sebastiani, Roberto (ed.)
2009Althaus, 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
2006Jacobs, 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
Hide details for Seiler, W.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
Hide details for Shankar, Natarajan (ed.)Shankar, Natarajan (ed.)
2006Sofronie-Stokkermans, VioricaAttachment IconInterpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250
Proceedings Article
1
Hide details for Sigayret, Alain (ed.)Sigayret, Alain (ed.)
2003Sofronie-Stokkermans, VioricaAttachment IconAutomated 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
Hide details for Sijanski, GrozdanaSijanski, Grozdana
2006Freiheit, 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
Hide details for Simon, CarloSimon, 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
Hide details for Slaney, John K. (ed.)Slaney, John K. (ed.)
1996Ganzinger, 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
Hide details for Slaney, J. K. (ed.)Slaney, J. K. (ed.)
1996Weidenbach, 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
1996Weidenbach, ChristophUnification in Pseudo-Linear Sort Theories is Decidable
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 343-357
Proceedings Article
75
Hide details for Sofronie-Stokkermans, VioricaSofronie-Stokkermans, Viorica
2013Sofronie-Stokkermans, VioricaHierarchical 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
2013Sofronie-Stokkermans, VioricaLocality and Applications to Subsumption Testing in EL and Some of its Extensions
In: Scientific Annals of Computer Science [23], 251-284
Journal Article
2013Horbach, Matthias
Sofronie-Stokkermans, Viorica
Obtaining Finite Local Theory Axiomatizations via Saturation
In: Frontiers of Combining Systems - 9th International Symposium, 198-213
Proceedings Article
2013Sofronie-Stokkermans, VioricaOn 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
2011Gasse, 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 automataReport
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
2010Sofronie-Stokkermans, VioricaAutomated 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 TopologiesReport
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
2010Sofronie-Stokkermans, VioricaHierarchical Reasoning for the Verification of Parametric Systems
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 171-187
Proceedings Article
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
On hierarchical reasoning in combinations of theoriesReport
2010Ihlemann, 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
2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
System Description: H-PILoT (Version 1.9)Report
2009Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica
Constraint Solving for InterpolationReport
2009Sofronie-Stokkermans, VioricaLocality results for certain extensions of theories with bridging functions
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 67-83
Proceedings Article
2009Sofronie-Stokkermans, VioricaReasoning in Complex Theories and Applications. Advanced Lecture
In: ESSLLI 2009 : European Summer School in Logic, Language and Information, 1-64
Electronic Proceedings Article
2009Sofronie-Stokkermans, VioricaSheaves and geometric logic and applications to modular verification of complex systems
In: Electronic Notes in Theoretical Computer Science [230], 161-187
Electronic Journal Article
2009Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
System Description: H-PILoT
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 131-139
Proceedings Article
2008Sofronie-Stokkermans, VioricaEfficient Hierarchical Reasoning about Functions over Numerical DomainsReport
2008Sofronie-Stokkermans, VioricaEfficient hierarchical reasoning about functions over numerical domains
In: KI 2008: Advances in Artificial Intelligence, 135-143
Proceedings Article
2008Sofronie-Stokkermans, VioricaInterpolation in local theory extensions
In: Logical Methods in Computer Science [4], 31 pages
Electronic Journal Article
2008Sofronie-Stokkermans, VioricaLocality 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
2008Sofronie-Stokkermans, VioricaLocality 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
2008Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica
On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281
Proceedings Article
2008Sofronie-Stokkermans, VioricaReasoning in Complex Theories and ApplicationsMiscellaneous
2008Sofronie-Stokkermans, VioricaSheaves and geometric logic and applications to modular verification of complex systemsReport
2007Sofronie-Stokkermans, VioricaAlgebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493
Part of a Book
2007Jacobs, Swen
Sofronie-Stokkermans, Viorica
Attachment IconApplications of hierarchical reasoning in the verification of complex systems
In: Electronic Notes in Theoretical Computer Science [174], 39-54
Electronic Journal Article
2007Sofronie-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
2007Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Automated reasoning in some local extensions of ordered structures
In: Proceedings of ISMVL 2007, Article1
Proceedings Article
2007Sofronie-Stokkermans, VioricaAttachment IconAutomated theorem proving by resolution in non-classical logics
In: Annals of Mathematics and Artificial Intelligence [49], 221-252
Journal Article
2007Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica
Constraint Solving for Interpolation
In: Verification, Model Checking and Abstract Interpretation : 8th International Conference, VMCAI 2007, 346-362
Proceedings Article
2007Sofronie-Stokkermans, VioricaHierarchical 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
2007Sofronie-Stokkermans, VioricaHierarchical 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
2007Sofronie-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
2007Sofronie-Stokkermans, VioricaAttachment IconOn unification for bounded distributive lattices
In: ACM Transactions on Computational Logic [8], 12.1-12.28
Journal Article
2007Sofronie-Stokkermans, VioricaOn 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
2006Jacobs, 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
2006Sofronie-Stokkermans, VioricaAutomatisches Beweisen in komplexen Theorien
In: MPG Jahrbuch [-],
Electronic Journal Article
2006Sofronie-Stokkermans, VioricaAttachment IconInterpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250
Proceedings Article
2006Sofronie-Stokkermans, VioricaLocal reasoning in verification
In: IJCAR'06 Workshop : VERIFY'06: Verification Workshop, 128-145
Electronic Proceedings Article
2006Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Waldmann, Uwe
Modular Proof Systems for Partial Functions with Evans Equality
In: Information and Computation [204], 1453-1492
Journal Article
2006Sofronie-Stokkermans, VioricaSheaves and geometric logic in concurrency
In: Proceedings of the Eighth Workshop on Geometric and Topological Methods in Concurrency (GETCO 2006), ?
Proceedings Article
2005Sofronie-Stokkermans, VioricaAttachment IconHierarchic reasoning in local theory extensions
In: Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 219-234
Proceedings Article
2004Sofronie-Stokkermans, VioricaAlgebraic and logical methods in automated theorem proving and in the study of concurrency
Universität des Saarlandes
Thesis - Habilitation thesis
2004Ganzinger, 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
2004Sofronie-Stokkermans, VioricaResolution-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
2003Sofronie-Stokkermans, VioricaAttachment IconAutomated 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
2003Sofronie-Stokkermans, VioricaAttachment IconRepresentation 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
2002Sofronie-Stokkermans, VioricaAttachment IconOn 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
2001Sofronie-Stokkermans, VioricaAttachment IconAutomated 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
2001Sofronie-Stokkermans, VioricaRepresentation 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
2000Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Attachment IconChaining 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
2000Sofronie-Stokkermans, VioricaAttachment IconDuality 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
2000Sofronie-Stokkermans, VioricaAttachment IconDuality 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
2000Sofronie-Stokkermans, VioricaAttachment IconOn unification for bounded distributive lattices
In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), 465-481
Proceedings Article
2000Sofronie-Stokkermans, VioricaAttachment IconPriestley 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
2000Sofronie-Stokkermans, VioricaAttachment IconResolution-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
2000Sofronie-Stokkermans, VioricaSome 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
1999Sofronie-Stokkermans, Viorica
[Stokkermans, Karel]
Attachment IconModeling Interaction by Sheaves and Geometric Logic
In: Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99), 512-523
Proceedings Article
1999Sofronie-Stokkermans, VioricaAttachment IconOn 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
1999Sofronie-Stokkermans, VioricaPriestley representation for distributive lattices with operators and applications to automated theorem proving
In: Dualities, Interpretability and Ordered Structures, 43-54
Proceedings Article
1999Sofronie-Stokkermans, VioricaRepresentation 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
1999Sofronie-Stokkermans, VioricaResolution-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
1998Sofronie-Stokkermans, VioricaOn 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
1998Sofronie-Stokkermans, VioricaRepresentation 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
1998Sofronie-Stokkermans, VioricaAttachment IconResolution-based Theorem Proving for SHn-LogicsReport
12
Hide details for Sofronie-Stokkermans, Viorica (ed.)Sofronie-Stokkermans, Viorica (ed.)
2011Automated Deduction - CADE-23 : 23rd International Conference on Automated DeductionProceedings
2011Frontiers of Combining SystemsProceedings
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
2010First-Order Theorem Proving : Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09)Electronic Proceedings
2009Lamotte-Schubert, Manuel
Weidenbach, Christoph
Attachment IconAnalysis 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
2009Lamotte-Schubert, Manuel
Weidenbach, Christoph
Analysis of Authorizations in SAP R/3
In: FTP 2009 : First-Order Theorem Proving, 90-104
Electronic Proceedings Article
2009First-Order Theorem Proving 2009Proceedings
2009First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving, ProceedingsProceedings
2009UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings
Electronic Proceedings
2008Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08)Proceedings
2008Jacobs, SwenAttachment IconIncremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62
Proceedings Article
2007Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07)Proceedings
1
Hide details for Spies, HendrikSpies, Hendrik
2003[Gaillourdet, Jean-Marie]
Hillenbrand, Thomas
[Löchner, Bernd]
[Spies, Hendrik]
Attachment IconThe New WALDMEISTER Loop at Work
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 317-321
Proceedings Article
1
Hide details for Stickel, Mark E. (ed.)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
Hide details for Stickel, Mark (ed.)Stickel, Mark (ed.)
2013Hillenbrand, 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
Hide details for Stokkermans, KarelStokkermans, Karel
1999Sofronie-Stokkermans, Viorica
[Stokkermans, Karel]
Attachment IconModeling Interaction by Sheaves and Geometric Logic
In: Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99), 512-523
Proceedings Article
1
Hide details for Stoyan, Herbert (ed.)Stoyan, Herbert (ed.)
1994Weidenbach, ChristophSorts, Resolution, Tableaux and Propositional Logic
In: KI-94 Workshops: Extended Abstracts, 315-316
Proceedings Article
4
Hide details for Sturm, ThomasSturm, Thomas
2013[Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas
Attachment IconPresburger 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
2011Sturm, 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
Hide details for Sturm, Thomas (ed.)Sturm, Thomas (ed.)
2013Košta, MarekSMT-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
2011Automated Deduction in Geometry : 7th International Workshop, ADG 2008Proceedings
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
Hide details for Sturm, T.Sturm, T.
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
Hide details for Suda, MartinSuda, Martin
2012Suda, Martin
Weidenbach, Christoph
Attachment IconA PLTL-prover based on labelled superposition with partial model guidance
In: Automated Reasoning : 6th International Joint Conference, IJCAR 2012, 537-543
Proceedings Article
2012Suda, Martin
Weidenbach, Christoph
Attachment IconLabelled Superposition for PLTL
In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, 391-405
Proceedings Article
2010Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick
On the Saturation of YAGOReport
2010Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick
On the Saturation of YAGO
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 441-456
Proceedings Article
2009Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard
Attachment IconExternal Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288
Proceedings Article
2009Weidenbach, 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
Hide details for Sutcliffe, GeoffSutcliffe, Geoff
2009Suda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard
Attachment IconExternal Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288
Proceedings Article
1
Hide details for Sutcliffe, Geoff (ed.)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
Hide details for Tang, Ching HooTang, Ching Hoo
2013[Dhungana, Deepak]
Tang, Ching Hoo
Weidenbach, Christoph
[Wischnewski, Patrick]
Attachment IconAutomated Verification of Interactive Rule-Based Configuration Systems
In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 551-561
Proceedings Article
1
Hide details for Teige, TeigeTeige, 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
Hide details for Teucke, AndreasTeucke, Andreas
2013Teucke, AndreasAttachment IconCDCL with Reduction
Universität des Saarlandes
Thesis - Masters thesis
2
Hide details for Theobalt, ChristianTheobalt, Christian
2002Weidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor
Attachment IconSPASS Version 2.0
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 275-279
Proceedings Article
1999Weidenbach, 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
Hide details for Tinelli, Cesare (ed.)Tinelli, Cesare (ed.)
2011Frontiers of Combining SystemsProceedings
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
Hide details for Tiwari, AshishTiwari, Ashish
2011Sturm, 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
Hide details for Tiwari, Ashish (ed.)Tiwari, Ashish (ed.)
2009UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings
Electronic Proceedings
2007Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07)Proceedings
2
Hide details for Topic, DaliborTopic, Dalibor
2007Weidenbach, Christoph
[Schmidt, Renate]
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor
Attachment IconSystem Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520
Proceedings Article
2006Hillenbrand, Thomas
Topic, Dalibor
Weidenbach, Christoph
Sudokus as Logical Puzzles
In: Disproving'06: Non-Theorems, Non-Validity, Non-Provability, 2-12
Proceedings Article
3
Hide details for Topić, DaliborTopić, Dalibor
2002Hillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor
Attachment IconIs 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
2002Weidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor
Attachment IconSPASS Version 2.0
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 275-279
Proceedings Article
1999Weidenbach, 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
Hide details for Tran, Duc-KhanhTran, Duc-Khanh
2009Tran, 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
Hide details for Turunen, Esko (ed.)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
2000Sofronie-Stokkermans, VioricaSome 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
Hide details for Vaida, Dragos (ed.)Vaida, Dragos (ed.)
2007Sofronie-Stokkermans, VioricaAlgebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493
Part of a Book
1
Hide details for Vaz de Carvalho, Júlia (ed.)Vaz de Carvalho, Júlia (ed.)
1999Sofronie-Stokkermans, VioricaPriestley representation for distributive lattices with operators and applications to automated theorem proving
In: Dualities, Interpretability and Ordered Structures, 43-54
Proceedings Article
1
Hide details for Veith, Helmut (ed.)Veith, Helmut (ed.)
2010Burel, GuillaumeEmbedding 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
Hide details for Vigneron, Laurent (ed.)Vigneron, Laurent (ed.)
2003Hillenbrand, ThomasAttachment IconCitius 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
Hide details for Viswanathan, Mahesh (ed.)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
Hide details for Vojtas, Peter (ed.)Vojtas, Peter (ed.)
1998Sofronie-Stokkermans, VioricaRepresentation 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
Hide details for Voronkov, AndreiVoronkov, Andrei
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]
Attachment IconOn the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271
Proceedings Article
1
Hide details for Voronkov, Andrei VoronkovVoronkov, Andrei Voronkov
2013Voronkov, Andrei Voronkov
Weidenbach, Christoph
Programming Logics - Essays in Memory of Harald GanzingerBook
15
Hide details for Voronkov, Andrei (ed.)Voronkov, Andrei (ed.)
2013Hillenbrand, 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
2013Sofronie-Stokkermans, VioricaOn combinations of local theory extensions
In: Programming Logics, Essays in Memory of Harald Ganzinger, 392-413
Part of a Book
2012Fietzke, 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
2012Suda, Martin
Weidenbach, Christoph
Attachment IconLabelled Superposition for PLTL
In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, 391-405
Proceedings Article
2010Horbach, MatthiasDisunification for Ultimately Periodic Interpretations
In: Logic for Programming, Artificial Intelligence, and Reasoning : 16th International Conference, LPAR-16, 290-311
Proceedings Article
2010Fietzke, 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
2006Ganzinger, Harald
[Korovin, Konstantin]
Theory Instantiation
In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06), 497-511
Proceedings Article
2002Weidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor
Attachment IconSPASS Version 2.0
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 275-279
Proceedings Article
2002Hillenbrand, Thomas
[Löchner, Bernd]
Attachment IconThe Next WALDMEISTER Loop
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 486-500
Proceedings Article
2001Weidenbach, ChristophCombining Superposition, Sorts and Splitting
In: Handbook of Automated Reasoning, 1965-2013
Part of a Book
2001Nonnengart, Andreas
Weidenbach, Christoph
Computing small clause normal forms
In: Handbook of Automated Reasoning, 335-367
Part of a Book
2001Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph
Attachment IconFirst-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
1999Waldmann, UweCancellative 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
Hide details for Waldmann, UweWaldmann, Uwe
2013Hillenbrand, 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
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[Baumgartner, Peter]
Waldmann, Uwe
A Combined Superposition and Model Evolution Calculus
In: Journal of Automated Reasoning [47], 191-227
Journal Article
Next Page