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: Download

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

FilenameSize (KB)Can be sorted ascendingAccessTypeAuthor(s) [non member]TitleYear
_03LICS.pdf136Public
Proceedings ArticleGanzinger, Harald
Korovin, Konstantin
New Directions in Instantiation-Based Theorem Proving
In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), 55-64
2003
_03CADE.2.ps211Public
Proceedings ArticleGanzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe
Superposition modulo a Shostak Theory
In: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, 182-196
2003
_00ISMVL_ps.gz55Public
Proceedings ArticleGanzinger, Harald
Sofronie-Stokkermans, Viorica
Chaining Techniques for Automated Theorem Proving in Many-Valued Logics
In: Proceedings of the 30th IEEE International Symposium on Multiple-Valued Logic (ISMVL-00), 337-344
2000
wm.ps393Intranet
Journal Article[Löchner, Bernd]
Hillenbrand, Thomas
A Phytography of WALDMEISTER
In: AI Communications [15], 127-133
2002
wmloop.ps386Public
Proceedings ArticleHillenbrand, Thomas
[Löchner, Bernd]
The Next WALDMEISTER Loop
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 486-500
2002
Weidenbach.pdf269Internal
Proceedings ArticleWeidenbach, Christoph
[Schmidt, Renate]
Hillenbrand, Thomas
Rusev, Rostislav
Topic, Dalibor
System Description: Spass Version 3.0
In: Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction, 514-520
2007
veiaspass.pdf762Public
Thesis - Master's thesisDreßler, ChristianAutomatic Analysis of Tree-Based Feature Models with SPASS
Universität des Saarlandes
2009
thesis.pdf278Intranet
Thesis - Master's thesisFietzke, ArnaudLabelled Splitting
Universität des Saarlandes
2007
thesis.pdf802Intranet
Thesis - Diploma thesisZimmer, StephanIntelligent Combination of a First Order Theorem Prover and SMT Procedures
Universität des Saarlandes
2007
thesis-final-publication-Germany.pdf1881Internal
Thesis - Doctoral dissertationLu, TianxiangFormal Verification of the Pastry Protocol
Universität des Saarlandes
2013
Thesis-Complete.pdf805Internal
Thesis - Master's thesisAzmy, NoranFormula Renaming with Generalizations
Universität des Saarlandes
2012
tableaux-2002.pdf241Public
Proceedings ArticleSofronie-Stokkermans, VioricaOn uniform word problems involving bridging operators on distributive lattices
In: Automated Reasoning with Analytic and Related Methods : International Conference, TABLEAUX 2002, 235-250
2002
superpositionLTL.pdf465Internal
Proceedings ArticleSuda, Martin
Weidenbach, Christoph
Labelled Superposition for PLTL
In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, 391-405
2012
superFixDom_TR.pdf333Public
ReportHorbach, Matthias
Weidenbach, Christoph
Superposition for Fixed Domains2009
SupDec.pdf952Public
Thesis - Doctoral dissertationHillenbrand, ThomasSuperposition and Decision Procedures -- Back and Forth
Universität des Saarlandes
2008
studia-logica-2000-2.pdf1351
807
Intranet
Journal ArticleSofronie-Stokkermans, VioricaDuality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. Part II
In: Studia Logica [64], 151-172
2000
studia-logica-2000-1.pdf1351Intranet
Journal ArticleSofronie-Stokkermans, VioricaDuality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. Part I
In: Studia Logica [64], 93-132
2000
studia-logica-2000-1.pdf1351
807
Intranet
Journal ArticleSofronie-Stokkermans, VioricaDuality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. Part II
In: Studia Logica [64], 151-172
2000
spass2002.ps106Public
Proceedings ArticleWeidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor
SPASS Version 2.0
In: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, 275-279
2002
sofronie-stokkermans-fct-1999.ps.gz92Public
Proceedings ArticleSofronie-Stokkermans, Viorica
[Stokkermans, Karel]
Modeling Interaction by Sheaves and Geometric Logic
In: Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99), 512-523
1999
sofronie-ijcar-06.pdf192Public
Proceedings ArticleSofronie-Stokkermans, VioricaInterpolation in local theory extensions
In: Proceedings of IJCAR 2006, 235-250
2006
sofronie-dam-revised.ps553Intranet
Journal ArticleSofronie-Stokkermans, VioricaAutomated theorem proving by resolution in non-classical logics
In: Annals of Mathematics and Artificial Intelligence [49], 221-252
2007
sofronie-cade2000.ps260Public
Proceedings ArticleSofronie-Stokkermans, VioricaOn unification for bounded distributive lattices
In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), 465-481
2000
sofronie-cade-2005.pdf518Public
Proceedings ArticleSofronie-Stokkermans, VioricaHierarchic reasoning in local theory extensions
In: Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 219-234
2005
sofronie-acm-tocl-final.pdf427Intranet
Journal ArticleSofronie-Stokkermans, VioricaOn unification for bounded distributive lattices
In: ACM Transactions on Computational Logic [8], 12.1-12.28
2007
SimonHirth.pdf402Intranet
Thesis - Master's thesisHirth, SimonAutomatische Analyse von DHCP und höheren Infrasturkturdiensten mit SPASS
Universität des Saarlandes
2006
SapR3.pdf300Public
Proceedings ArticleLamotte-Schubert, Manuel
Weidenbach, Christoph
Analysis of Authorizations in SAP R/3
In: First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving proceedings, 90-104
2009
rcdcl.pdf407Internal
Thesis - Master's thesisTeucke, AndreasCDCL with Reduction
Universität des Saarlandes
2013
Quantifier_Elimination.pdf656Internal
Thesis - Master's thesisReuter, JochenReal Linear Quantifier Elimination
Universität des Saarlandes
2013
pwm.ps110Public
Proceedings Article[Gaillourdet, Jean-Marie]
Hillenbrand, Thomas
[Löchner, Bernd]
[Spies, Hendrik]
The New WALDMEISTER Loop at Work
In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, 317-321
2003
proofdoc.pdf371Intranet
Thesis - Bachelor thesis[Dressler, Christian]First-Order Proof Documentation
Universität des Saarlandes
2007
paper.pdf466Public
Proceedings Article[Dhungana, Deepak]
Tang, Ching Hoo
Weidenbach, Christoph
[Wischnewski, Patrick]
Automated Verification of Interactive Rule-Based Configuration Systems
In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 551-561
2013
NOSup.ps104Public
Electronic Proceedings ArticleHillenbrand, ThomasA Superposition View on Nelson-Oppen
In: Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning, 16-20
2004
next-wm-loop.ps244
Proceedings ArticleHillenbrand, Thomas
[Löchner, Bernd]
The Next WALDMEISTER Loop (Extended Abstract)
In: Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001, 13-21
2001
mvl-book-02.ps375Public
Part of a BookSofronie-Stokkermans, VioricaRepresentation Theorems and the Semantics of Non-classical Logics, and Applications to Automated Theorem Proving
In: Beyond Two: Theory and Applications of Multiple Valued Logic, 59-100
2003
MPI-I-2008-RG1-001.pdf319Intranet
ReportHirth, Simon
Karl, Carsten
Weidenbach, Christoph
Automatic Analysis of LAN Infrastructures2007
MPI-I-2008-RG1-001.pdf361Public
ReportFietzke, Arnaud
Weidenbach, Christoph
Labelled Splitting2008
MPI-I-2007-RG1-002.pdf262Intranet
ReportHillenbrand, Thomas
Weidenbach, Christoph
Superposition for Finite Domains2007
mcpastry-lu-avocs2010.pdf98Public
Proceedings ArticleLu, Tianxiang
[Merz, Stephan]
Weidenbach, Christoph
Model Checking the Pastry Routing Protocol
In: 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), 19-21
2010
master.pdf339Intranet
Thesis - Master's thesisWischnewski, PatrickContextual Rewriting in SPASS
Universität des Saarlandes
2007
master.pdf1341Intranet
Thesis - Master's thesisLamotte, ManuelAnalysis of Authorizations in SAP R/3
Fachhochschule Trier
2008
MasterThesis_Claudia_Esquivel.pdf756Internal
Thesis - Master's thesisEsquivel Pinto, Claudia So fiaComputing Variable Orders for SAT-Problems
Universität des Saarlandes
2013
MasterThesis.pdf465Intranet
Thesis - Master's thesisRusev, RostislavBitvector Reasoning with SPASS
Universität des Saarlandes
2008
Kruglov.PhD.2013.pdf2139Internal
Thesis - Doctoral dissertationKruglov, EvgenySuperposition Modulo Theory
Universität des Saarlandes
2013
ki2009.pdf167Public
Proceedings ArticleSuda, Martin
[Sutcliffe, Geoff]
Wischnewski, Patrick
Lamotte-Schubert, Manuel
de Melo, Gerard
External Sources of Axioms in Automated Theorem Proving
In: KI 2009: Advances in Artificial Intelligence, 281-288
2009
jim-03-sofronie.ps.gz126Public
Proceedings ArticleSofronie-Stokkermans, VioricaAutomated theorem proving by resolution in non-classical logics
In: Fourth International Conference Journees de l'Informatique Messine: Knowledge Discovery and Discrete Mathematics (JIM-03), 151-167
2003
j-mvl-2001.ps.gz221Intranet
Journal ArticleSofronie-Stokkermans, VioricaAutomated Theorem Proving by Resolution for Finitely-Valued Logics Based on Distributive Lattices with Operators
In: Multiple-Valued Logic - An International Journal [6], 289-344
2001
j-mvl-2000.ps337Intranet
Journal ArticleSofronie-Stokkermans, VioricaPriestley Duality for SHn-algebras and Applications to the Study of Kripke-style Models for SHn-logics
In: Multiple-Valued Logic - An International Journal [5], 281-305
2000
InstGen.pdf196Intranet
Electronic Journal ArticleJacobs, Swen
Waldmann, Uwe
Comparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78
2006
InstGen.pdf196Intranet
Journal ArticleJacobs, Swen
Waldmann, Uwe
Comparing Instance Generation Methods for Automated Reasoning
In: Journal of Automated Reasoning [38], 57-78
2007
InstGen-final.pdf428Public
Proceedings ArticleJacobs, Swen
Waldmann, Uwe
Comparing Instance Generation Methods for Automated Reasoning
In: Automated Reasoning with Analytic Tableaux and Related Methods : International Conference, TABLEAUX 2005, 153-168
2005
ijcar2012_submission_81.pdf389Internal
Proceedings ArticleSuda, Martin
Weidenbach, Christoph
A PLTL-prover based on labelled superposition with partial model guidance
In: Automated Reasoning : 6th International Joint Conference, IJCAR 2012, 537-543
2012
IIGLR.pdf200Public
Proceedings ArticleJacobs, SwenIncremental Instance Generation in Local Reasoning
In: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08, 47-62
2008
IIGLR.pdf209Public
Proceedings ArticleJacobs, SwenIncremental Instance Generation in Local Reasoning
In: Computer Aided Verification : 21st International Conference, CAV 2009, 368-382
2009
gjoin.ps264Public
Journal Article[Avenhaus, Jürgen]
Hillenbrand, Thomas
[Löchner, Bernd]
On Using Ground Joinable Equations in Equational Theorem Proving
In: Journal of Symbolic Computation [36], 217-233
2003
ftp98-lncs-selection.pdf253Public
Proceedings ArticleSofronie-Stokkermans, VioricaResolution-based theorem proving for SHn-logics
In: Automated Deduction in Classical and Non-Classical Logic (Selected Papers of FTP'98), 268-282
2000
ftp-98.pdf253Intranet
ReportSofronie-Stokkermans, VioricaResolution-based Theorem Proving for SHn-Logics1998
frocos-paper.pdf591Internal
Proceedings Article[Karrenberg, Ralf]
Košta, Marek
Sturm, Thomas
Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
In: Frontiers of Combining Systems, 56-70
2013
evaluation.ps171
Proceedings Article[Nieuwenhuis, Robert]
Hillenbrand, Thomas
[Riazanov, Alexandre]
[Voronkov, Andrei]
On the Evaluation of Indexing Techniques for Theorem Proving
In: Automated reasoning : First International Joint Conference, IJCAR 2001, 257-271
2001
entcs-pdpar06-jacobs-sofronie.pdf337Internal
Electronic Journal ArticleJacobs, Swen
Sofronie-Stokkermans, Viorica
Applications of hierarchical reasoning in the verification of complex systems
In: Electronic Notes in Theoretical Computer Science [174], 39-54
2007
diss.pdf1158Public
Thesis - Doctoral dissertationIhlemann, CarstenReasoning in Combinations of Theories
Universität des Saarlandes
2010
dissertation_wischnewski.pdf859Internal
Thesis - Doctoral dissertationWischnewski, PatrickEfficient Reasoning Procedures for Complex First-Order Theories
Universität des Saarlandes
2012
diplom-2006-03-13.pdf2462Public
Thesis - Diploma thesisBankstahl, JanNetflow analysis of SAP R/3 traffic in an enterprise environment
Universität des Saarlandes
2006
decIndQueries_TR.pdf390Public
ReportHorbach, Matthias
Weidenbach, Christoph
Deciding the Inductive Validity of Forall Exists* Queries2009
DDD+2010.pdf339Intranet
Electronic Journal Article[Damm, Werner]
[Dierks, Henning]
[Disch, Stefan]
Hagemann, Willem
[Pigorsch, Florian]
[Scholl, Christoph]
Waldmann, Uwe
[Wirtz, Boris]
Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces
In: Science of Computer Programming [in press], 1-29
2011
citius.ps357Public
Electronic Proceedings ArticleHillenbrand, ThomasCitius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER
In: Proceedings of the 4th International Workshop on First Order Theorem Proving, FTP'03, 1-13
2003
CarstenKarl.PDF1101Intranet
Thesis - Master's thesisKarl, CarstenAutomatische Analyse von Layer 3 Netzwerken mit SPASS
Universität des Saarlandes
2006
cade-99.pdf248Public
Proceedings ArticleSofronie-Stokkermans, VioricaOn the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results
In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 157-171
1999
BaThesis.pdf200Intranet
Thesis - Bachelor thesisDimova, DilyanaPropositional Abduction
Universität des Saarlandes
2007
ba-thesis.pdf493Internal
Thesis - Bachelor thesisBromberger, MartinAdapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic
Universität des Saarlandes
2012
AtomFinal.ps547
Proceedings ArticleAfshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph
First-Order Atom Definitions Extended
In: Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001), 309-319
2001
art%3A10.1007%2Fs11786-012-0135-4-1.pdf410Internal
Journal ArticleKruglov, Evgeny
Weidenbach, Christoph
Superposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456
2012
analysis.ps81Public
Proceedings ArticleHillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor
Is Logic Effective for Analyzing C Programs?
In: Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, 27-30
2002
10-1.1007_s11786-012-0135-4.pdf436Internal
Journal ArticleKruglov, Evgeny
Weidenbach, Christoph
Superposition Decides the First-Order Logic Fragment Over Ground Theories
In: Mathematics in Computer Science [6], 427-456
2012

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