VSL 2014: VIENNA SUMMER OF LOGIC 2014

A
Ansótegui, Carlos	The Fractal Dimension of SAT Formulas
B
Baumgartner, Peter	Finite Quantification in Hierarchic Theorem Proving
Bax, Joshua	Finite Quantification in Hierarchic Theorem Proving
Beeson, Michael	Otter proofs of theorems in Tarskian geometry
Berdine, Josh	Computing All Implied Equalities via SMT-based Partition Refinement
Beyersdorff, Olaf	The Complexity of Theorem Proving in Circumscription and Minimal Entailment
Biere, Armin	A Unified Proof System for QBF Preprocessing
Bjorner, Nikolaj	Computing All Implied Equalities via SMT-based Partition Refinement
Blanchette, Jasmin Christian	Unified Classical Logic Completeness: A Coinductive Pearl
Bonet, Maria Luisa	The Fractal Dimension of SAT Formulas
Boudou, Joseph	Skeptik [System Description]
Bozzelli, Laura	Visibly Linear Temporal Logic
Brockschmidt, Marc	Proving Termination of Programs Automatically with AProVE Proving Termination and Memory Safety for Programs with Pointer Arithmetic
C
Carral, David	EL-ifying Ontologies
Cerrito, Serenella	Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+
Ceylan, İsmail İlkan	The Bayesian Description Logic BEL
Chew, Leroy	The Complexity of Theorem Proving in Circumscription and Minimal Entailment
Chocron, Paula	A Gentle Non-Disjoint Combination of Satisfiability Procedures
Cuenca Grau, Bernardo	EL-ifying Ontologies
D
David, Amélie	Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+
Dixon, Clare	Clausal Resolution for Modal Logics of Confluence
E
Echenim, Mnacho	A Rewriting Strategy to Generate Prime Implicates in Equational Logic
Ehlers, Rüdiger	A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic
Emmes, Fabian	Proving Termination of Programs Automatically with AProVE
F
Feier, Cristina	EL-ifying Ontologies
Fellner, Andreas	Skeptik [System Description]
Fontaine, Pascal	A Gentle Non-Disjoint Combination of Satisfiability Procedures
Frohn, Florian	Proving Termination of Programs Automatically with AProVE Proving Termination and Memory Safety for Programs with Pointer Arithmetic
Fuhs, Carsten	Proving Termination of Programs Automatically with AProVE Proving Termination and Memory Safety for Programs with Pointer Arithmetic
G
Giesl, Jürgen	Proving Termination of Programs Automatically with AProVE Proving Termination and Memory Safety for Programs with Pointer Arithmetic
Giráldez-Cru, Jesus	The Fractal Dimension of SAT Formulas
Glimm, Birte	Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures
Goranko, Valentin	Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+
Gore, Rajeev	And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL Implementing Tableaux Calculi Using BDDs: BDDTab System Description A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description
Gorin, Daniel	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description)
H
Hensel, Jera	Proving Termination and Memory Safety for Programs with Pointer Arithmetic
Hetzl, Stefan	Introducing quantified cuts in logic with equality
Heule, Marijn	A Unified Proof System for QBF Preprocessing
Hitzler, Pascal	EL-ifying Ontologies
Horbach, Matthias	Locality Transfer: From Constrained Axiomatizations to Reachability Predicates
Horrocks, Ian	EL-ifying Ontologies
J
Jeannin, Jean-Baptiste	dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems
K
Koopmann, Patrick	Count and Forget: Uniform Interpolation of SHQ-Ontologies
L
Lahav, Ori	SAT-based Decision Procedure for Analytic Pure Sequent Calculi
Lange, Martin	A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic
Leitsch, Alexander	Introducing quantified cuts in logic with equality
Lellmann, Bjoern	Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications
Levy, Jordi	The Fractal Dimension of SAT Formulas
Liebig, Thorsten	Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures
Lima, Leonardo	Quati: An Automated Tool for Proving Permutation Lemmas
Lindblad, Fredrik	A Focused Sequent Calculus for Higher-Order Logic
M
Marcos, João	Clausal Resolution for Modal Logics of Confluence
McMillan, Kenneth	Structured Search and Learning
N
Nalon, Cláudia	Clausal Resolution for Modal Logics of Confluence
Nigam, Vivek	Quati: An Automated Tool for Proving Permutation Lemmas
O
Olesen, Kerry	Implementing Tableaux Calculi Using BDDs: BDDTab System Description
Olivetti, Nicola	NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics
Otten, Jens	MleanCoP: A Connection Prover for First-Order Modal Logic
Otto, Carsten	Proving Termination of Programs Automatically with AProVE
P
Papacchini, Fabio	Terminating Minimal Model Generation Procedures for Propositional Modal Logics
Pattinson, Dirk	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description)
Pease, Adam	Knowledge Engineering for Large Ontologies with Sigma KEE 3.0
Peltier, Nicolas	A Rewriting Strategy to Generate Prime Implicates in Equational Logic
Peñaloza, Rafael	The Bayesian Description Logic BEL
Platzer, André	dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems
Plücker, Martin	Proving Termination of Programs Automatically with AProVE
Popescu, Andrei	Unified Classical Logic Completeness: A Coinductive Pearl
Pozzato, Gian Luca	NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics
R
Reis, Giselle	Introducing quantified cuts in logic with equality Quati: An Automated Tool for Proving Permutation Lemmas
Ringeissen, Christophe	A Gentle Non-Disjoint Combination of Satisfiability Procedures
Ruemmer, Philipp	Approximations for Model Construction
S
Sanchez, Cesar	Visibly Linear Temporal Logic
Schmidt, Renate A.	Count and Forget: Uniform Interpolation of SHQ-Ontologies Terminating Minimal Model Generation Procedures for Propositional Modal Logics
Schneider-Kamp, Peter	Proving Termination of Programs Automatically with AProVE Proving Termination and Memory Safety for Programs with Pointer Arithmetic
Schröder, Lutz	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description)
Schulz, Stephan	Knowledge Engineering for Large Ontologies with Sigma KEE 3.0
Seidl, Martina	A Unified Proof System for QBF Preprocessing
Sofronie-Stokkermans, Viorica	Locality Transfer: From Constrained Axiomatizations to Reachability Predicates
Steigmiller, Andreas	Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures
Stroeder, Thomas	Proving Termination of Programs Automatically with AProVE Proving Termination and Memory Safety for Programs with Pointer Arithmetic
Stump, Aaron	StarExec: a Cross-Community Infrastructure for Logic Solving
Sutcliffe, Geoff	StarExec: a Cross-Community Infrastructure for Logic Solving
Swiderski, Steffi	Proving Termination of Programs Automatically with AProVE
T
Tapolczai, Janos	Introducing quantified cuts in logic with equality
Thiemann, Rene	Proving Termination of Programs Automatically with AProVE
Thomson, Jimmy	Implementing Tableaux Calculi Using BDDs: BDDTab System Description A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description
Tinelli, Cesare	StarExec: a Cross-Community Infrastructure for Logic Solving
Tourret, Sophie	A Rewriting Strategy to Generate Prime Implicates in Equational Logic
Traytel, Dmitriy	Unified Classical Logic Completeness: A Coinductive Pearl
W
Waldmann, Uwe	Finite Quantification in Hierarchic Theorem Proving
Weller, Daniel	Introducing quantified cuts in logic with equality
Widmann, Florian	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description)
Wintersteiger, Christoph M.	Approximations for Model Construction
Wißmann, Thorsten	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description)
Woltzenlogel Paleo, Bruno	Skeptik [System Description]
Wos, Larry	Otter proofs of theorems in Tarskian geometry
Wu, Jesse	A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description
Z
Zeljić, Aleksandar	Approximations for Model Construction
Zhang, Wenhui	QBF Encoding of Temporal Properties and QBF-Based Verification
Zohar, Yoni	SAT-based Decision Procedure for Analytic Pure Sequent Calculi

Disclaimer | Powered by EasyChair Smart Program