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: 4. BibTeX Citation Keys

Login to this database


 

Previous Page | Next Page | Expand All | Collapse All | Search (Full Text)
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

BibTeX cite keyAuthor/EditorYearTitleType
AfshordelHillenbrandWeidenbach01Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph
2001Attachment 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
AlthausEtAlFrocos2009Althaus, Ernst
Kruglov, Evgeny
Weidenbach, Christoph
2009Superposition Modulo Linear Arithmetic SUP(LA)
In: Frontiers of Combining Systems : 7th International Symposium, FroCoS 2009, 84-99
Proceedings Article
AvenhausHillenbrandLoechner2003Avenhaus, Jürgen
Hillenbrand, Thomas
Löchner, Bernd
2003Attachment IconOn Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233
Journal Article
Azmy12Azmy, Noran2012Attachment IconFormula Renaming with Generalizations
Universität des Saarlandes
Thesis - Masters thesis
BachmairGanzinger-94-jlcBachmair, Leo
Ganzinger, Harald
1994Rewrite-based equational theorem proving with selection and simplification
In: Journal of Logic and Computation [4], 217-247
Journal Article
BachmairGanzingerWaldmann-92-alpBachmair, Leo
Ganzinger, Harald
Waldmann, Uwe
1992Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434
Proceedings Article
BachmairGanzingerWaldmann-93-kgsBachmair, Leo
Ganzinger, Harald
Waldmann, Uwe
1993Superposition with simplification as a decision procedure for the monadic class with equality
In: Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC'93, 83-96
Proceedings Article
BachmairGanzingerWaldmann-93-licsBachmair, Leo
Ganzinger, Harald
Waldmann, Uwe
1993Set Constraints are the Monadic Class
In: Eighth Annual IEEE Symposium on Logic in Computer Science, 75-83
Proceedings Article
BachmairGanzingerWaldmann-94-aaeccBachmair, Leo
Ganzinger, Harald
Waldmann, Uwe
1994Refutational Theorem Proving for Hierarchic First-Order Theories
In: Applicable Algebra in Engineering, Communication and Computing (AAECC) [5], 193-212
Journal Article
Bankstahl06Bankstahl, Jan2006Attachment IconNetflow analysis of SAP R/3 traffic in an enterprise environment
Universität des Saarlandes
Thesis - other
Bankstahl2006Bankstahl, Jan2006Netflow analysis of SAP R/3 traffic in an enterprise
Universität des Saarlandes
Thesis - Masters thesis
Bastuck2006Bastuck, Andrea2006Maschinell unterstützte Analyse eines Sicherheitsprotokolls
Universität des Saarlandes
Thesis - other
BaumgartnerWaldmann2009CADEBaumgartner, Peter
Waldmann, Uwe
2009Superposition and Model Evolution Combined
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 17-34
Proceedings Article
BaumgartnerWaldmann2011Baumgartner, Peter
Waldmann, Uwe
2011A Combined Superposition and Model Evolution Calculus
In: Journal of Automated Reasoning [47], 191-227
Journal Article
Bromberger12Bromberger, Martin2012Attachment IconAdapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic
Universität des Saarlandes
Thesis - Bachelor thesis
Burel2010Burel, Guillaume2010Embedding Deduction Modulo into a Prover
In: Computer Science Logic : 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, 155-169
Proceedings Article
Burel2010aBurel, Guillaume2011Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
In: Logical Methods in Computer Science [7], 3:1-3:31
Electronic Journal Article
Damm-Ihlemann-Sofronie-Stokkermans2011Damm, Werner
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
2011Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata
In: HSCC'11 : Proceedings of the 2011 ACM/SIGBED Hybrid Systems: Computation and Control, 73-82
Proceedings Article
Damm-Ihlemann-Sofronie-Stokkermans2011-mscDamm, Werner
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
2011PTIME parametric verification of safety properties for reasonable linear hybrid automata
In: Mathematics in Computer Science [5], 469-497
Journal Article
Damm-Ihlemann-Sofronie-Stokkermans2011-reportDamm, Werner
Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
2011PTIME parametric verification of safety properties for reasonable linear hybrid automataReport
DammDierksDischEtAl2011Damm, Werner
Dierks, Henning
Disch, Stefan
Hagemann, Willem
Pigorsch, Florian
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris
2011Attachment 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
DammDierksDischEtAl2012Damm, Werner
Dierks, Henning
Disch, Stefan
Hagemann, Willem
Pigorsch, Florian
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris
2012Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
In: Science of Computer Programming [77], 1122-1150
Journal Article
DammDierksHagemannEtAl2011Damm, Werner
Disch, Stefan
Hagemann, Willem
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris
2011Integrating incremental flow pipes into a symbolic model checker for hybrid systemsReport
DammDischHungarJacobsPangPigorschSchollWaldmannWirtz2007Damm, Werner
Disch, Stefan
Hungar, Hardi
Jacobs, Swen
Pang, Jun
Pigorsch, Florian
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris
2007Exact 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
DammDischHungarPangPigorschSchollWaldmannWirtz2006Damm, Werner
Disch, Stefan
Hungar, Hardi
Pang, Jun
Pigorsch, Florian
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris
2006Automatic 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
Dhungana2013Dhungana, Deepak
Tang, Ching Hoo
Weidenbach, Christoph
Wischnewski, Patrick
2013Attachment IconAutomated Verification of Interactive Rule-Based Configuration Systems
In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 551-561
Proceedings Article
Dimova09Dimova, Dilyana2009On the Translation of Timed Automata into First-order Logic
Universität des Saarlandes
Thesis - Masters thesis
Dimova2007Dimova, Dilyana2007Attachment IconPropositional Abduction
Universität des Saarlandes
Thesis - Bachelor thesis
Dressler09Dreßler, Christian2009Attachment IconAutomatic Analysis of Tree-Based Feature Models with SPASS
Universität des Saarlandes
Thesis - Masters thesis
Dressler2007Dressler, Christian2007Attachment IconFirst-Order Proof Documentation
Universität des Saarlandes
Thesis - Bachelor thesis
ErramiEiswirth:13aErrami, H.
Eiswirth, M.
Grigoriev. D.
Seiler, W.
Sturm, T.
Weber, A.
2013Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates
In: Proceedings of the CASC 2013, 88-99
Proceedings Article
Esquivel13Esquivel Pinto, Claudia So fia2013Attachment IconComputing Variable Orders for SAT-Problems
Universität des Saarlandes
Thesis - Masters thesis
faber-ihlemann-jacobs-sofronie-2010-reportFaber, Johannes
Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica
2010Automatic Verification of Parametric Specifications with Complex TopologiesReport
faber-ihlemann-jacobs-sofronieStokkermans-ifm-2010Faber, Johannes
Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica
2010Automatic Verification of Parametric Specifications with Complex Topologies
In: Integrated Formal Methods : 8th International Conference, IFM 2010, 152-167
Proceedings Article
faber-jacobs-sofronie-ifm-2007Faber, Johannes
Jacobs, Swen
Sofronie-Stokkermans, Viorica
2007Verifying CSP-OZ-DC specifications with complex data types and timing parameters
In: Proceedings of IFM 2007: Integrated Formal Methods, 233-252
Proceedings Article
Fehreretal94aFehrer, Detlef
Hustadt, Ullrich
Jaeger, Manfred
Nonnengart, Andreas
Ohlbach, Hans Jürgen
Schmidt, Renate A.
Weidenbach, Christoph
Weydert, Emil
1994Description Logics for Natural Language Processing
In: International Workshop on Description Logics '94, 80-84
Proceedings Article
Fietzke2007Fietzke, Arnaud2007Attachment IconLabelled Splitting
Universität des Saarlandes
Thesis - Masters thesis
FietzkeKruglovWeidenbach2012Fietzke, Arnaud
Kruglov, Evgeny
Weidenbach, Christoph
2012Automatic 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
FietzkeWeidenbach09Fietzke, Arnaud
Weidenbach, Christoph
2009Labelled Splitting
In: Annals of Mathematics and Artificial Intelligence [55], 3-34
Journal Article
FietzkeWeidenbach2008Fietzke, Arnaud
Weidenbach, Christoph
2008Attachment IconLabelled SplittingReport
FietzkeWeidenbach2010Fietzke, Arnaud
Hermanns, Holger
Weidenbach, Christoph
2010Superposition-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
FietzkeWeidenbach2011Fietzke, Arnaud
Weidenbach, Christoph
2011Superposition as a Decision Procedure for Timed Automata
In: Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2011),
Proceedings Article
FietzkeWeidenbachCADE08Fietzke, Arnaud
Weidenbach, Christoph
2008Labelled Splitting
In: IJCAR, 459-474
Proceedings Article
FietzkeWeidenbachMCS2012Fietzke, Arnaud
Weidenbach, Christoph
2012Superposition as a Decision Procedure for Timed Automata
In: Mathematics in Computer Science [6], 409-425
Electronic Journal Article
FontaineMerzWeidenbach12Fontaine, Pascal
Merz, Stephan
Weidenbach, Christoph
2012Combination of Disjoint Theories: Beyond Decidability
In: Proceedings of the 6th International Joint Conference on Automated Reasoning,
Proceedings Article
Freiheit2005Freiheit, Jörn
Luuk, Marc
Münch, Susanne
Sijanski, Grozdana
Zangl, Fabrice
2006Lexecute: Visualisation and representation of legal procedures
In: Digital Evidence Journal [3], 17-27
Journal Article
Freiheit2005bFreiheit, Jörn
Zangl, Fabrice
2006Model-based user-interface management for public services
In: 6th European Conference on e-Government, 141-151
Proceedings Article
Freiheit2005cLilith, Nimrod
Billington, Jonathan
Freiheit, Jörn
2006Approximate 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
Freiheit2005dSimon, Carlo
Freiheit, Jörn
Olbrich, Sebastian
2006Using BPEL processes defined by Event-driven Process Chains
In: 5. GI-Workshop "EPK 2006 - Geschäftsprozessmanagement mit Ereignisgesteuerten Prozessketten", 121-135
Proceedings Article
Freiheit2007aFreiheit, Jörn
Zangl, Fabrice
2007Model-based User-interface Management for Public Services
In: Electronic Journal of e-Government [5], 53-62
Journal Article
Freiheit2007cZiemann, Joerg
Matheis, Thomas
Freiheit, Jörn
2007Modelling of Cross-Organizational Business Processes - Current Methods and Standards
In: Enterprise Modelling and Information Systems Architectures [2], 23-31
Journal Article
Freiheit2007dZiemann, Joerg
Matheis, Thomas
Freiheit, Jörn
2007Modelling of Cross-Organizational Business Processes
In: Enterprise Modelling and Information Systems Architectures 2007, 87-95
Proceedings Article
ftp09Peltier, Sofronie-Stokkermans (ed.)2009First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving, ProceedingsProceedings
GaillourdetHillenbrandLoechner2003Gaillourdet, Jean-Marie
Hillenbrand, Thomas
Löchner, Bernd
Spies, Hendrik
2003Attachment IconThe New WALDMEISTER Loop at Work
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 317-321
Proceedings Article
GanKor:ThInst:2006Ganzinger, Harald
Korovin, Konstantin
2006Theory Instantiation
In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06), 497-511
Proceedings Article
Ganzinger-94-satGanzinger, Harald1994The Saturate SystemUnpublished/Draft
Ganzinger-SofronieStokkermans-Waldmann-ijcar-2004Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Waldmann, Uwe
2004Modular Proof Systems for Partial Functions with Weak Equality
In: Automated reasoning : Second International Joint Conference, IJCAR 2004, 168-182
Proceedings Article
GanzingerHillenbrandWaldmann2003Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe
2003Attachment IconSuperposition modulo a Shostak Theory
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 182-196
Proceedings Article
GanzingerKorovin-03-licsGanzinger, Harald
Korovin, Konstantin
2003Attachment IconNew Directions in Instantiation-Based Theorem Proving
In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), 55-64
Proceedings Article
GanzingerMeyerWeidenbach-97-cadeGanzinger, Harald
Meyer, Christoph
Weidenbach, Christoph
1997Soft Typing for Ordered Resolution
In: Proceedings of the 14th International Conference on Automated Deduction (CADE-14), 321-335
Proceedings Article
GanzingerSofronie-Stokkermans-00-ismvlGanzinger, Harald
Sofronie-Stokkermans, Viorica
2000Attachment 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
GanzingerWaldmann-92-ctrsGanzinger, Harald
Waldmann, Uwe
1992Termination 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
GanzingerWaldmann1996CADEGanzinger, Harald
Waldmann, Uwe
1996Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 388-402
Proceedings Article
Gasse-Sofronie-Stokkermans-dl2011Gasse, Francis
Sofronie-Stokkermans, Viorica
2011Efficient TBox Subsumption Checking in Combinations of EL and (fragments of) FL0
In: Proceedings of the 2011 International Workshop on Description Logics (DL-2011), 125-135
Electronic Proceedings Article
GSW-i-and-cGanzinger, Harald
Sofronie-Stokkermans, Viorica
Waldmann, Uwe
2006Modular Proof Systems for Partial Functions with Evans Equality
In: Information and Computation [204], 1453-1492
Journal Article
HaehnleKerberEtAl96Hähnle, Reiner
Kerber, Manfred
Weidenbach, Christoph
1996Common Syntax of the DFG-Schwerpunktprogramm ``Deduktion''Report
Hillenbrand2003Hillenbrand, Thomas2003Attachment 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
Hillenbrand2004Hillenbrand, Thomas2004Attachment 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
HillenbrandDiss2008Hillenbrand, Thomas2008Attachment IconSuperposition and Decision Procedures -- Back and Forth
Universität des Saarlandes
Thesis - PhD thesis
HillenbrandEtAl2006DisprovingHillenbrand, Thomas
Topic, Dalibor
Weidenbach, Christoph
2006Sudokus as Logical Puzzles
In: Disproving'06: Non-Theorems, Non-Validity, Non-Provability, 2-12
Proceedings Article
HillenbrandLoechner2001Hillenbrand, Thomas
Löchner, Bernd
2001Attachment IconThe Next WALDMEISTER Loop (Extended Abstract)
In: Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001, 13-21
Proceedings Article
HillenbrandPiskacWaldmannWeidenbach2011Hillenbrand, Thomas
Piskac, Ruzica
Waldmann, Uwe
Weidenbach, Christoph
2013From Search to Computation: Redundancy Criteria and Simplification at Work
In: Programming Logics, Essays in Memory of Harald Ganzinger, ?
Part of a Book
HillenbrandWeidenbach13Hillenbrand, Thomas
Weidenbach, Christoph
2013Superposition for Bounded Domains
In: Automated Reasoning and Mathematics, Essays in Memory of William W. McCune, 68-100
Part of a Book
HillenbrandWeidenbach2007ReportHillenbrand, Thomas
Weidenbach, Christoph
2007Attachment IconSuperposition for Finite DomainsReport
Hirt2006Hirth, Simon2006Attachment IconAutomatische Analyse von DHCP und höheren Infrasturkturdiensten mit SPASS
Universität des Saarlandes
Thesis - Masters thesis
HirthKarlWeidenbach2007reportHirth, Simon
Karl, Carsten
Weidenbach, Christoph
2007Attachment IconAutomatic Analysis of LAN InfrastructuresReport
HL02-CADE18Hillenbrand, Thomas
Löchner, Bernd
2002Attachment IconThe Next WALDMEISTER Loop
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 486-500
Proceedings Article
Horbach2009TR1Horbach, Matthias
Weidenbach, Christoph
2009Attachment IconDeciding the Inductive Validity of Forall Exists* QueriesReport
Horbach2009TR2Horbach, Matthias
Weidenbach, Christoph
2009Attachment IconSuperposition for Fixed DomainsReport
Horbach2010Horbach, Matthias2010Disunification for Ultimately Periodic Interpretations
In: Logic for Programming, Artificial Intelligence, and Reasoning : 16th International Conference, LPAR-16, 290-311
Proceedings Article
Horbach2010PhDHorbach, Matthias2010Superposition-based Decision Procedures for Fixed Domain and Minimal Model Semantics
Universität des Saarlandes
Thesis - PhD thesis
Horbach2013InformatikHorbach, Matthias2013INFORMATIK 2013 - Informatik angepasst an Mensch, Organisation und UmweltBook
Horbach2013McCuneKapur, Deepak
Zhang, Zhihai
Horbach, Matthias
Zhao, Hantao
Lu, Qi
Nguyen, ThanhVu
2014Geometric 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
HorbachWeidenbach2009CADEHorbach, Matthias
Weidenbach, Christoph
2009Decidability Results for Saturation-Based Model Building
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 404-420
Proceedings Article
HorbachWeidenbach2010Horbach, Matthias
Weidenbach, Christoph
2010Superposition for Fixed Domains
In: ACM Transactions on Computational Logic [11], 27,1-27,35
Journal Article
HorbachWeidenbachCSL08Horbach, Matthias
Weidenbach, Christoph
2008Superposition for Fixed Domains
In: CSL, 293-307
Proceedings Article
HorbachWeidenbachCSL09Horbach, Matthias
Weidenbach, Christoph
2009Deciding 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
hpilot2009Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
2009System Description: H-PILoT
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 131-139
Proceedings Article
HPT02Hillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor
2002Attachment 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
HSW1998Hustadt, Ullrich
Schmidt, Renate A.
Weidenbach, Christoph
1998Optimised Functional Translation and Resolution
In: Proceedings of the International Conference on Automated Reaso ning with Analytic Tableaux and Related Methods (TABLEAUX'98), 36-37
Proceedings Article
ihlemann-jacobs-sofronie-tacas2008Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica
2008On local reasoning in verification
In: Proceedings of TACAS 2008, 265-281
Proceedings Article
Ihlemann-Sofronie-Stokkermans-atr60-2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
2010On hierarchical reasoning in combinations of theoriesReport
Ihlemann-Sofronie-Stokkermans-atr61-2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
2010System Description: H-PILoT (Version 1.9)Report
Ihlemann-Sofronie-Stokkermans-ijcar-2010Ihlemann, Carsten
Sofronie-Stokkermans, Viorica
2010On Hierarchical Reasoning in Combinations of Theories
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 30-45
Proceedings Article
IhlemannDiss2010Ihlemann, Carsten2010Attachment IconReasoning in Combinations of Theories
Universität des Saarlandes
Thesis - PhD thesis
jacobs-sofronie-pdpar-06Jacobs, Swen
Sofronie-Stokkermans, Viorica
2006Applications of hierarchical reasoning in the verification of complex systems
In: PDPAR'06: Pragmatical Aspects of Decision Procedures in Automated Reasoning, 15-26
Electronic Proceedings Article
jacobs-sofronie-pdpar-entcsJacobs, Swen
Sofronie-Stokkermans, Viorica
2007Attachment IconApplications of hierarchical reasoning in the verification of complex systems
In: Electronic Notes in Theoretical Computer Science [174], 39-54
Electronic Journal Article
Jacobs2008Jacobs, Swen2008Attachment IconIncremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62
Proceedings Article
Jacobs2009Jacobs, Swen2009Attachment IconIncremental Instance Generation in Local Reasoning
In: Computer Aided Verification : 21st International Conference, CAV 2009, 368-382
Proceedings Article
JacobsDiss2010Jacobs, Swen2010Hierarchic Decision Procedures for Verification
Universität des Saarlandes
Thesis - PhD thesis
JacobsWaldmann2005Jacobs, Swen
Waldmann, Uwe
2005Attachment IconComparing Instance Generation Methods for Automated Reasoning
In: Automated Reasoning with Analytic Tableaux and Related Methods : International Conference, TABLEAUX 2005, 153-168
Proceedings Article
JacobsWaldmann2006Jacobs, Swen
Waldmann, Uwe
2006Attachment IconComparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78
Electronic Journal Article
JacobsWaldmann2007Jacobs, Swen
Waldmann, Uwe
2007Attachment IconComparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78
Journal Article
JacquemardMeyerWeidenbach98Jacquemard, Florent
Meyer, Christoph
Weidenbach, Christoph
1998Unification in Extensions of Shallow Equational Theories
In: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), 76-90
Proceedings Article
Karl2006Karl, Carsten2006Attachment IconAutomatische Analyse von Layer 3 Netzwerken mit SPASS
Universität des Saarlandes
Thesis - Masters thesis
KarrenbergKostaSturm2013Karrenberg, Ralf
Košta, Marek
Sturm, Thomas
2013Attachment IconPresburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70
Proceedings Article
Kosta2013Košta, Marek2013SMT-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
Kruglov2008Kruglov, Evgeny2008Superposition Modulo Linear Arithmetic
Universität des Saarlandes
Thesis - Masters thesis
KruglovDiss13Kruglov, Evgeny2013Attachment IconSuperposition Modulo Theory
Universität des Saarlandes
Thesis - PhD thesis
KruglovFroCoS2011Eggers, Andreas
Kruglov, Evgeny
Kupferschmid, Stefan
Scheibler, Karsten
Teige, Teige
Weidenbach, Christoph
2011SUP(NLA) -- Combining Superposition and Non-Linear Arithmetic
In: 8th International Symposium on Frontiers of Combining Systems, 119-134
Proceedings Article
KruglovMACIS2011Kruglov, Evgeny
Weidenbach, Christoph
2011SUP(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
KruglovWeidenbachMCS2012Kruglov, Evgeny
Weidenbach, Christoph
2012Attachment IconSuperposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456
Journal Article
KruglovWeidenbachMCS2012eKruglov, Evgeny
Weidenbach, Christoph
2012Attachment IconSuperposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456
Journal Article
Lamotte-SchubertWeidenbachFTP09Lamotte-Schubert, Manuel
Weidenbach, Christoph
2009Attachment 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
Lamotte-SchubertWeidenbachFTP09CEURLamotte-Schubert, Manuel
Weidenbach, Christoph
2009Analysis of Authorizations in SAP R/3
In: FTP 2009 : First-Order Theorem Proving, 90-104
Electronic Proceedings Article
LAMOTTE2008Lamotte, Manuel2008Attachment IconAnalysis of Authorizations in SAP R/3
Fachhochschule Trier
Thesis - Masters thesis
LasarukSturm:11aLasaruk, Aless
Sturm, Thomas
2011Automatic 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
LetzWeidenbach98Letz, Reinhold
Weidenbach, Christoph
1998Paradigmen 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
LevAmiWeidenbachEtAl2007CADELev-Ami, Tal
Weidenbach, Christoph
Reps, Thomas
Sagiv, Mooly
2007Labelled Clauses
In: 21st International Conference on Automated Deduction (CADE-21), 311-327
Proceedings Article
LoechnerHillenbrandAICOM2002Löchner, Bernd
Hillenbrand, Thomas
2002Attachment IconA Phytography of WALDMEISTER
In: AI Communications [15], 127-133
Journal Article
LuDiss13Lu, Tianxiang2013Attachment IconFormal Verification of the Pastry Protocol
Universität des Saarlandes
Thesis - PhD thesis
LudwigDipl2006Ludwig, Michel2006Extensions of the Knuth-Bendix Ordering with LPO-like Properties
Universität des Saarlandes
Thesis - Masters thesis
LudwigWaldmann2007Ludwig, Michel
Waldmann, Uwe
2007An 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
LuTlaPastryForte2011Lu, Tianxiang
Merz, Stephan
Weidenbach, Christoph
2011Towards 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
LuTX2009Lu, Tianxiang
Merz, Stephan
Weidenbach, Christoph
2010Attachment IconModel Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21
Proceedings Article
Neumann09Neumann, Stephan Rouven2009Automated Proof Generation of Possibiltiy Properties in Inductive Protocol Verification
Universität des Saarlandes
Thesis - Bachelor thesis
NieuwenhuisHillenbrandRiazanovVoronkov2001Nieuwenhuis, Robert
Hillenbrand, Thomas
Riazanov, Alexandre
Voronkov, Andrei
2001Attachment IconOn the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271
Proceedings Article
NonnengartRockWeidenbach98Nonnengart, Andreas
Rock, Georg
Weidenbach, Christoph
1998On Generating Small Clause Normal Forms
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 397-411
Proceedings Article
NonnengartWeidenbach2001handbookNonnengart, Andreas
Weidenbach, Christoph
2001Computing small clause normal forms
In: Handbook of Automated Reasoning, 335-367
Part of a Book
OhlbachWeidenbach95Ohlbach, Hans Jürgen
Weidenbach, Christoph
1995A Note on Assumptions about Skolem Functions
In: Journal of Automated Reasoning [15], 267-275
Journal Article
Peltier-Sofronie-Stokkermans-ftpceur-2010Peltier, Sofronie-Stokkermans (ed.)2009First-Order Theorem Proving 2009Proceedings
PrevostoWaldmann2006Prevosto, Virgile
Waldmann, Uwe
2006SPASS+T
In: ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 18-33
Proceedings Article
Reuter13Reuter, Jochen2013Attachment IconReal Linear Quantifier Elimination
Universität des Saarlandes
Thesis - Masters thesis
RusevMaster2008Rusev, Rostislav2008Attachment IconBitvector Reasoning with SPASS
Universität des Saarlandes
Thesis - Masters thesis
Rybalchenko-Sofronie-Stokkermans-2009Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica
2009Constraint Solving for InterpolationReport
Rybalchenko-Sofronie-vmcai07Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica
2007Constraint Solving for Interpolation
In: Verification, Model Checking and Abstract Interpretation : 8th International Conference, VMCAI 2007, 346-362
Proceedings Article
Sofronie-cade-05Sofronie-Stokkermans, Viorica2005Attachment IconHierarchic reasoning in local theory extensions
In: Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 219-234
Proceedings Article
Sofronie-getco06-entcsSofronie-Stokkermans, Viorica2009Sheaves and geometric logic and applications to modular verification of complex systems
In: Electronic Notes in Theoretical Computer Science [230], 161-187
Electronic Journal Article
sofronie-ihlemann-ismvl-2007Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
2007Automated reasoning in some local extensions of ordered structures
In: Proceedings of ISMVL 2007, Article1
Proceedings Article
Sofronie-Ihlemann-Jacobs-dagstuhl07Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Jacobs, Swen
2007Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
In: Deduction and Decision Procedures, 1-22
Electronic Proceedings Article
sofronie-ihlemann-jmvl-2007Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
2007Automated reasoning in some local extensions of ordered structures
In: Journal of Multiple-Valued Logic and Soft Computing [13], 397-414
Journal Article
Sofronie-ijcar-06Sofronie-Stokkermans, Viorica2006Attachment IconInterpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250
Proceedings Article
Sofronie-Stokkermans-2010-jscRybalchenko, Andrey
Sofronie-Stokkermans, Viorica
2010Constraint Solving for Interpolation
In: Journal of Symbolic Computation [45], 1212-1233
Journal Article
Sofronie-Stokkermans-2013Sofronie-Stokkermans, Viorica2013Hierarchical reasoning and model generation for the verification of parametric hybrid systems
In: Proceedings of the 24th International Conference on Automated Deduction (CADE-24), 360-376
Proceedings Article
Sofronie-Stokkermans-addct07Ghilardi, Sattler, Sofronie-Stokkermans, Tiwari (ed.)2007Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07)Proceedings
Sofronie-Stokkermans-aiml2008Sofronie-Stokkermans, Viorica2008Locality and subsumption testing in $\mathcalEL$ and some of its extensions
In: Advances in Modal Logic, Vol.7 (Proceedings of AIML 2008), 315-339
Proceedings Article
Sofronie-Stokkermans-atr45-2008Sofronie-Stokkermans, Viorica2008Efficient Hierarchical Reasoning about Functions over Numerical DomainsReport
Sofronie-Stokkermans-atr46-2008Sofronie-Stokkermans, Viorica2008Sheaves and geometric logic and applications to modular verification of complex systemsReport
Sofronie-Stokkermans-cade-2011Bjørner, Sofronie-Stokkermans (ed.)2011Automated Deduction - CADE-23 : 23rd International Conference on Automated DeductionProceedings
Sofronie-Stokkermans-cade09Sofronie-Stokkermans, Viorica2009Locality results for certain extensions of theories with bridging functions
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 67-83
Proceedings Article
Sofronie-Stokkermans-cade2000Sofronie-Stokkermans, Viorica2000Attachment IconOn unification for bounded distributive lattices
In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), 465-481
Proceedings Article
Sofronie-Stokkermans-cedar2008Baader, Ghilardi, Hermann, Sattler, Sofronie-Stokkermans (ed.)2008Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08)Proceedings
Sofronie-Stokkermans-ceur2010Peltier, Sofronie-Stokkermans (ed.)2010First-Order Theorem Proving : Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09)Electronic Proceedings
Sofronie-Stokkermans-dagstuhl-2010Sofronie-Stokkermans, Viorica2010Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms-
In: Interaction versus Automation : the two Faces of Deduction, 1-33
Electronic Proceedings Article
Sofronie-Stokkermans-dam-06Sofronie-Stokkermans, Viorica2007Attachment IconAutomated theorem proving by resolution in non-classical logics
In: Annals of Mathematics and Artificial Intelligence [49], 221-252
Journal Article
Sofronie-Stokkermans-dl2008Sofronie-Stokkermans, Viorica2008Locality and subsumption testing in $\mathcalEL$ and some of its extensions
In: Proceedings of the 21st International Workshop on Description Logics (DL-2008), 11pages
Electronic Proceedings Article
Sofronie-Stokkermans-dualities1999Sofronie-Stokkermans, Viorica1999Priestley representation for distributive lattices with operators and applications to automated theorem proving
In: Dualities, Interpretability and Ordered Structures, 43-54
Proceedings Article
Sofronie-Stokkermans-esslli09Sofronie-Stokkermans, Viorica2009Reasoning in Complex Theories and Applications. Advanced Lecture
In: ESSLLI 2009 : European Summer School in Logic, Language and Information, 1-64
Electronic Proceedings Article
Sofronie-Stokkermans-frocos-07Sofronie-Stokkermans, Viorica2007Hierarchical and modular reasoning in complex theories: The case of local theory extensions
In: Frontiers of Combining Systems. 6th International Symposium FroCos 2007, Proceedings, 47-71
Proceedings Article
Sofronie-Stokkermans-frocos-2011Tinelli, Sofronie-Stokkermans (ed.)2011Frontiers of Combining SystemsProceedings
Sofronie-Stokkermans-frocos2013Horbach, Matthias
Sofronie-Stokkermans, Viorica
2013Obtaining Finite Local Theory Axiomatizations via Saturation
In: Frontiers of Combining Systems - 9th International Symposium, 198-213
Proceedings Article
Sofronie-Stokkermans-ftp07-abstractSofronie-Stokkermans, Viorica2007Hierarchical and modular reasoning in complex theories: The case of local theory extensions.
In: Proceedings of the Sixth International Workshop on First-Order Theorem Proving (FTP 2007), 1
Proceedings Article
Sofronie-Stokkermans-ftp2000Sofronie-Stokkermans, Viorica2000Attachment 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
Sofronie-Stokkermans-getco-06Sofronie-Stokkermans, Viorica2006Sheaves and geometric logic in concurrency
In: Proceedings of the Eighth Workshop on Geometric and Topological Methods in Concurrency (GETCO 2006), ?
Proceedings Article
Sofronie-Stokkermans-hab04Sofronie-Stokkermans, Viorica2004Algebraic and logical methods in automated theorem proving and in the study of concurrency
Universität des Saarlandes
Thesis - Habilitation thesis
Sofronie-Stokkermans-ismvl-2004Sofronie-Stokkermans, Viorica2004Resolution-based decision procedures for the positive theory of some finitely generated varieties of algebras
In: Proceedings of the 34th International Symposium on Multiple-Valued Logic (ISMVL-2004), 32-37
Proceedings Article
Sofronie-Stokkermans-jahrbuch-2006Sofronie-Stokkermans, Viorica2006Automatisches Beweisen in komplexen Theorien
In: MPG Jahrbuch [-],
Electronic Journal Article
Sofronie-Stokkermans-jim-2003Sofronie-Stokkermans, Viorica2003Attachment 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
Sofronie-Stokkermans-ki2008Sofronie-Stokkermans, Viorica2008Efficient hierarchical reasoning about functions over numerical domains
In: KI 2008: Advances in Artificial Intelligence, 135-143
Proceedings Article
Sofronie-Stokkermans-lmcs-2008Sofronie-Stokkermans, Viorica2008Interpolation in local theory extensions
In: Logical Methods in Computer Science [4], 31 pages
Electronic Journal Article
Sofronie-Stokkermans-moisil-08Sofronie-Stokkermans, Viorica2007Algebraic and logical methods in computer science: some aspects
In: Grigore C. Moisil and his followers, 488-493
Part of a Book
Sofronie-Stokkermans-mvl-2003Sofronie-Stokkermans, Viorica2003Attachment 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
Sofronie-Stokkermans-sacs2013Sofronie-Stokkermans, Viorica2013Locality and Applications to Subsumption Testing in EL and Some of its Extensions
In: Scientific Annals of Computer Science [23], 251-284
Journal Article
Sofronie-Stokkermans-tableaux-2002Sofronie-Stokkermans, Viorica2002Attachment 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
Sofronie-Stokkermans-tutorial-ki08Sofronie-Stokkermans, Viorica2008Reasoning in Complex Theories and ApplicationsMiscellaneous
Sofronie-Stokkermans-unif-05Sofronie-Stokkermans, Viorica2007Attachment IconOn unification for bounded distributive lattices
In: ACM Transactions on Computational Logic [8], 12.1-12.28
Journal Article
Sofronie-Stokkermans1999Sofronie-Stokkermans, Viorica2001Attachment 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
Sofronie-Stokkermans1999-cadeSofronie-Stokkermans, Viorica1999Attachment 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
Sofronie-Stokkermans1999-fctSofronie-Stokkermans, Viorica
Stokkermans, Karel
1999Attachment IconModeling Interaction by Sheaves and Geometric Logic
In: Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99), 512-523
Proceedings Article
Sofronie-Stokkermans1999-ismvlSofronie-Stokkermans, Viorica1999Representation Theorems and Automated Theorem Proving in Non-Classical Logics
In: Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic (ISMVL-99), 242-247
Proceedings Article
Sofronie-Stokkermans1999-lmpsSofronie-Stokkermans, Viorica1999Resolution-based theorem proving for non-classical logics based on distributive lattices with operators
In: Proceedings of the 11th International Congress of Logic, Methodology and Philosophy of Science. Volume of abstracts, 481-481
Proceedings Article
Sofronie-Stokkermans2000-atlas-1Iturrioz, Luisa
Sofronie-Stokkermans, Viorica
2000SHn-algebras (Symmetric Heyting algebras of order n)
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-11
Part of a Book
Sofronie-Stokkermans2000-atlas-2Sofronie-Stokkermans, Viorica2000Some properties of Kleene algebras
In: COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, 1-7
Part of a Book
Sofronie-Stokkermans2001-ismvlSofronie-Stokkermans, Viorica2001Representation theorems and the semantics of (semi)lattice-based logics
In: Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logics, 125-134
Proceedings Article
Sofronie-Stokkermans2006Sofronie-Stokkermans, Viorica2007On unification in certain finitely generated varieties of algebras
In: Proceedings of the 21th International Workshop on Unification (UNIF 2007), 1-5
Electronic Proceedings Article
Sofronie-Stokkermans2009-addct-unifLynch, Narendran, Baader, Ghilardi, Hermann, Sofronie-Stokkermans, Tiwari (ed.)2009UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings
Electronic Proceedings
Sofronie-Stokkermans2009-jsc-addctGhilardi, Silvio
Sattler, Ulrike
Sofronie-Stokkermans, Viorica
Tiwari, Ashish
2010Special issue on automated deduction: Decidability, complexity, tractability
In: Journal of Symbolic Computation [45], 151-152
Journal Article
Sofronie-Stokkermans2010-ijcarSofronie-Stokkermans, Viorica2010Hierarchical Reasoning for the Verification of Parametric Systems
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 171-187
Proceedings Article
Sofronie-Stokkermans2012-jsc-ftpPeltier, Nicolas
Sofronie-Stokkermans, Viorica
2012First-order theorem proving: Foreword
In: Journal of Symbolic Computation [47], 1009-1010
Journal Article
Sofronie-Stokkermans2013-jar-cade-special-issueBjorner, Nikolaj
Sofronie-Stokkermans, Viorica
2013Preface: Special Issue of Selected Extended Papers of CADE-23
In: Journal of Automated Reasoning [51], 1-2
Journal Article
Sofronie-verify-06Sofronie-Stokkermans, Viorica2006Local reasoning in verification
In: IJCAR'06 Workshop : VERIFY'06: Verification Workshop, 128-145
Electronic Proceedings Article
Sofronie-wlphg11Sofronie-Stokkermans, Viorica2013On combinations of local theory extensions
In: Programming Logics, Essays in Memory of Harald Ganzinger, 392-413
Part of a Book
Sofronie1997aSofronie-Stokkermans, Viorica2000Attachment 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
Sofronie1997bSofronie-Stokkermans, Viorica2000Attachment 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
Sofronie1997cSofronie-Stokkermans, Viorica2000Attachment 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
Sofronie1998aSofronie-Stokkermans, Viorica1998On 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
Sofronie1998bSofronie-Stokkermans, Viorica1998Attachment IconResolution-based Theorem Proving for SHn-LogicsReport
Sofronie1998cSofronie-Stokkermans, Viorica1998Representation Theorems and Automated Theorem Proving in Certain Classes of Non-Classical Logics
In: Proceedings of the Workshop on Many-Valued Logic for AI Applications (ECAI-98), ?-?
Proceedings Article
SturmTiwari:11aSturm, Thomas
Tiwari, Ashish
2011Verification and Synthesis Using Real Quantifier Elimination
In: ISSAC 2011 : Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation, 329-336
Proceedings Article
SturmZengler2011Sturm, Zengler (ed.)2011Automated Deduction in Geometry : 7th International Workshop, ADG 2008Proceedings
Suda2010Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick
2010On the Saturation of YAGOReport
SudaSutcliffeWischnewskiLamotteKI2009Suda, Martin
Sutcliffe, Geoff
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard
2009Attachment IconExternal Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288
Proceedings Article
SudaWeidenbachIJCAR2012Suda, Martin
Weidenbach, Christoph
2012Attachment IconA PLTL-prover based on labelled superposition with partial model guidance
In: Automated Reasoning : 6th International Joint Conference, IJCAR 2012, 537-543
Proceedings Article
SudaWeidenbachLPAR2012Suda, Martin
Weidenbach, Christoph
2012Attachment IconLabelled Superposition for PLTL
In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, 391-405
Proceedings Article
SudaWeidenbachWischnewskiIJCAR10Suda, Martin
Weidenbach, Christoph
Wischnewski, Patrick
2010On the Saturation of YAGO
In: Automated Reasoning : 5th International Joint Conference, IJCAR 2010, 441-456
Proceedings Article
Teucke13Teucke, Andreas2013Attachment IconCDCL with Reduction
Universität des Saarlandes
Thesis - Masters thesis
tran-atva08Lynch, Christopher
Tran, Duc-Khanh
2008SMELS: Satisfiability Modulo Equality with Lazy Superposition
In: Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008, 186-200
Proceedings Article
tran-decproc-jscTran, Duc-Khanh
Ringeissen, Christopher
Ranise, Silvio
Kirchner, Helene
2009Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation
In: Journal of Symbolic Computation [45-], 261-286
Journal Article
VoronkovetAl13Kapur, Deepak
Nieuwenhuis, Robert
Voronkov, Andrei
Weidenbach, Christoph
Wilhelm, Reinhard
2013Harald Ganzinger's Legacy: Contributions to Logics and Programming
In: Programming Logics,
Proceedings Article
VoronkovWeidenbach13Voronkov, Andrei Voronkov
Weidenbach, Christoph
2013Programming Logics - Essays in Memory of Harald GanzingerBook
Waldmann1997Waldmann, Uwe1997Cancellative Abelian Monoids in Refutational Theorem Proving
Universität des Saarlandes
Thesis - PhD thesis
Waldmann1997FTPWaldmann, Uwe1997A 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
Waldmann1998Waldmann, Uwe1998Superposition for Divisible Torsion-Free Abelian Groups
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 144-159
Proceedings Article
Waldmann1998IPLWaldmann, Uwe1998Extending reduction orderings to ACU-compatible reduction orderings
In: Information Processing Letters [67], 43-49
Journal Article
Waldmann1999LPARWaldmann, Uwe1999Cancellative 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
Waldmann2001IJCARWaldmann, Uwe2001Superposition and Chaining for Totally Ordered Divisible Abelian Groups (Extended Abstract)
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 226-241
Proceedings Article
Waldmann2002aJSCWaldmann, Uwe2002Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I)
In: Journal of Symbolic Computation [33], 777-829
Journal Article
Waldmann2002bJSCWaldmann, Uwe2002Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II)
In: Journal of Symbolic Computation [33], 831-861
Journal Article
Waldmann2002IUCWaldmann, Uwe2002A New Input Technique for Accented Letters in Alphabetical Scripts
In: Proceedings of the 20th International Unicode Conference, C12
Proceedings Article
Waldmann92aWaldmann, Uwe1992Semantics of Order-Sorted Specifications
In: Theoretical Computer Science [94], 1-35
Journal Article
Wand2012Blanchette, Jasmin Christian
Popescu, Andrei
Wand, Daniel
Weidenbach, Christoph
2012More SPASS with Isabelle : Superposition with Hard Sorts and Configurable Simplification
In: Interactive Theorem Proving : Third International Conference, ITP 2012, 345-360
Proceedings Article
WBH+02-CADE18Weidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor
2002Attachment IconSPASS Version 2.0
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 275-279
Proceedings Article
WeberSturm:11aWeber, Andreas
Sturm, Thomas
Abdel-Rahman, Essam O.
2011Algorithmic Global Criteria for Excluding Oscillations
In: Bulletin of Mathematical Biology [73], 899-916
Journal Article
Weidenbach1999jarWeidenbach, Christoph1999SPASS V0.95TPTP
In: Journal of Automated Reasoning [23], 21-21
Journal Article
Weidenbach2000habilWeidenbach, Christoph2000Entscheidbarkeitsprobleme für monadische (Horn)Klauselklassen
Universität des Saarlandes, Naturwissenschaftlich-Technische Fakultät
Thesis - Habilitation thesis
Weidenbach2001handbookWeidenbach, Christoph2001Combining Superposition, Sorts and Splitting
In: Handbook of Automated Reasoning, 1965-2013
Part of a Book
Weidenbach92aWeidenbach, Christoph1993A New Sorted Logic
In: GWAI-92: Advances in Artificial Inteligence, Proceedings 16th German Workshop on Artificial Intelligence, 43-54
Proceedings Article
Weidenbach93aWeidenbach, Christoph1993Extending the Resolution Method with Sorts
In: Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI '93), 60-65
Proceedings Article
Weidenbach94aWeidenbach, Christoph1994First-Order Tableaux with Sorts
In: TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 247-261
Proceedings Article
Weidenbach94cWeidenbach, Christoph1994Sorts, Resolution, Tableaux and Propositional Logic
In: KI-94 Workshops: Extended Abstracts, 315-316
Proceedings Article
Weidenbach95dWeidenbach, Christoph1995First-Order Tableaux with Sorts
In: Journal of the Interest Group in Pure and Applied Logics [3], 887-906
Journal Article
Weidenbach95eBarth, Peter
Kleine Büning, Hans
Weidenbach, Christoph
1995Workshop CPL Computational Propositional Logic
In: KI-95 Activities: Workshops, Posters, Demos, 71-72
Proceedings Article
Weidenbach96aWeidenbach, Christoph1996Unification in Pseudo-Linear Sort Theories is Decidable
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 343-357
Proceedings Article
Weidenbach96bWeidenbach, Christoph
Gaede, Bernd
Rock, Georg
1996SPASS & FLOTTER, Version 0.42
In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), 141-145
Proceedings Article
Weidenbach96cWeidenbach, Christoph1996Unification in Sort Theories
In: Proceedings of the 10th International Workshop on Unification, UNIF'96, 16-25
Proceedings Article
Weidenbach96dWeidenbach, Christoph1996Sorted Unification and Its Application to Automated Theorem Proving
In: Proceedings of the CADE-13 Workshop: Term Schematizations and Their Applications, 67-76
Proceedings Article
Weidenbach96eWeidenbach, Christoph1996Computational Aspects of a First-Order Logic with Sorts
Universität des Saarlandes
Thesis - PhD thesis
Weidenbach96fWeidenbach, Christoph1996Unification in Sort Theories and its Applications
In: Annals of Mathematics and Artificial Intelligence [18], 261-293
Journal Article
Weidenbach97jarWeidenbach, Christoph1997SPASS Version 0.49
In: Journal of Automated Reasoning [18], 247-252
Journal Article
Weidenbach98kluwerWeidenbach, Christoph1998Sorted Unification and Tree Automata
In: Automated Deduction - A Basis for Applications, 291-320
Part of a Book
Weidenbach98teubnerWeidenbach, Christoph1998Rechnen in sortierter Prädikatenlogik
In: Ausgezeichnete Informatikdissertationen 1997, 183-197
Part of a Book
Weidenbach99cadeWeidenbach, Christoph1999Towards 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
Weidenbach99cadespassWeidenbach, Christoph
Afshordel, Bijan
Brahm, Uwe
Cohrs, Christian
Engel, Thorsten
Keen, Enno
Theobalt, Christian
Topić, Dalibor
1999System Description: SPASS Version 1.0.0
In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 314-318
Proceedings Article
WeidenbachEtAlSpass2009Weidenbach, Christoph
Dimova, Dilyana
Fietzke, Arnaud
Suda, Martin
Wischnewski, Patrick
2009SPASS Version 3.5
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 140-145
Proceedings Article
WeidenbachMeyerEtAl98jarWeidenbach, Christoph
Meyer, Christoph
Cohrs, Christian
Engel, Thorsten
Keen, Enno
1998SPASS V0.77
In: Journal of Automated Reasoning [21], 113-113
Journal Article
WeidenbachSchmidtEtAl2007cadeWeidenbach, Christoph
Schmidt, Renate
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor
2007Attachment IconSystem Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520
Proceedings Article
WeidenbachWischnewski2012Weidenbach, Christoph
Wischnewski, Patrick
2012Satisfiability Checking and Query Answering for large Ontologies
In: PAAR-2012 : Third Workshop on Practical Aspects of Automated Reasoning, 163-177
Electronic Proceedings Article
WeidenbachWischnewskiAICom10Weidenbach, Christoph
Wischnewski, Patrick
2010Subterm Contextual Rewriting
In: AI Communications [23], 97-109
Journal Article
WeidenbachWischnewskiCADE08Weidenbach, Christoph
Wischnewski, Patrick
2008Contextual Rewriting in SPASS
In: PAAR/ESHOL, 115-124
Proceedings Article
WeidenbachWischnewskiReport2009Weidenbach, Christoph
Wischnewski, Patrick
2009Contextual RewritingReport
Wischnewski12Wischnewski, Patrick2012Attachment IconEfficient Reasoning Procedures for Complex First-Order Theories
Universität des Saarlandes
Thesis - PhD thesis
Wischnewski2007Wischnewski, Patrick2007Attachment IconContextual Rewriting in SPASS
Universität des Saarlandes
Thesis - Masters thesis
Zimmer2007Zimmer, Stephan2007Attachment IconIntelligent Combination of a First Order Theorem Prover and SMT Procedures
Universität des Saarlandes
Thesis - other

Previous Page | Next Page | Expand All | Collapse All | Search (Full Text)