Vienna Summer of Logic

IJCAR 2014 Accepted Papers

Jasmin Christian Blanchette, Andrei Popescu and Dmitriy TraytelUnified Classical Logic Completeness: A Coinductive Pearl
Ori Lahav and Yoni ZoharSAT-based Decision Procedure for Analytic Pure Sequent Calculi
Serenella Cerrito, Amélie David and Valentin GorankoOptimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+
Sophie Tourret, Mnacho Echenim and Nicolas PeltierA Rewriting Strategy to Generate Prime Implicates in Equational Logic
Wenhui ZhangQBF Encoding of Temporal Properties and QBF-Based Verification
Olaf Beyersdorff and Leroy ChewThe Complexity of Theorem Proving in Circumscription and Minimal Entailment
Patrick Koopmann and Renate A. SchmidtCount and Forget: Uniform Interpolation of SHQ-Ontologies
Cláudia Nalon, João Marcos and Clare DixonClausal Resolution for Modal Logics of Confluence
İsmail İlkan Ceylan and Rafael PeñalozaThe Bayesian Description Logic BEL
Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai and Daniel WellerIntroducing quantified cuts in logic with equality
Bruno Woltzenlogel Paleo, Joseph Boudou and Andreas FellnerSkeptik [System Description]
Vivek Nigam, Giselle Reis and Leonardo LimaQuati: An Automated Tool for Proving Permutation Lemmas
Nicola Olivetti and Gian Luca PozzatoNESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics
Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Stroeder, Steffi Swiderski and Rene ThiemannProving Termination of Programs Automatically with AProVE
Thomas Stroeder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel and Peter Schneider-KampAutomated Termination Analysis for Programs with Pointer Arithmetic
Marijn Heule, Martina Seidl and Armin BiereUnified Proof System for QBF Preprocessing
Rajeev Gore, Jimmy Thomson and Jesse Wu A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description
Adam Pease and Stephan SchulzKnowledge Engineering for Large Ontologies with Sigma KEE 3.0
Rajeev Gore, Jimmy Thomson and Kerry OlesenImplementing Tableaux Calculi Using BDDs: BDDTab System Description
Peter Baumgartner, Joshua Bax and Uwe WaldmannFinite Quantification in Hierarchic Theorem Proving
Rüdiger Ehlers and Martin LangeAn Incremental Approximation to the Finite Satisfiability Problem for Full Interval Temporal Logic
Bjoern Lellmann Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications
Carlos Ansótegui, Maria Luisa Bonet, Jesus Giráldez-Cru and Jordi LevyThe Fractal Dimension of SAT Formulas
Laura Bozzelli and Cesar SanchezVisibly Linear Temporal Logic
Andreas Steigmiller, Birte Glimm and Thorsten LiebigCoupling Tableau Algorithms for Expressive Description Logics with Completion-based Saturation Procedures
Josh Berdine and Nikolaj BjornerComputing All Implied Equalities via SMT-based Partition Refinement
Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp RuemmerApproximations for Model Construction
Fabio Papacchini and Renate A. SchmidtTerminating Minimal Model Generation Procedures for Propositional Modal Logics
Paula Chocron, Pascal Fontaine and Christophe RingeissenA Gentle Non-Disjoint Combination of Satisfiability Procedures
Aaron Stump, Geoff Sutcliffe and Cesare TinelliStarExec: a Cross-Community Infrastructure for Logic Solving
Fredrik LindbladA Focused Sequent Calculus for Higher-Order Logic
Matthias Horbach and Viorica Sofronie-StokkermansLocality Transfer: From Constrained Axiomatizations to Reachability Predicates
Daniel Gorin, Dirk Pattinson, Lutz Schröder, Thorsten Wißmann and Florian WidmannCOOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description)
David Carral, Cristina Feier, Bernardo Cuenca Grau, Pascal Hitzler and Ian HorrocksEL-ifying Ontologies
Jens OttenMleanCoP: A Connection Prover for First-Order Modal Logic
Michael Beeson and Larry WosOtter proofs of theorems in Tarskian geometry
Jean-Baptiste Jeannin and André PlatzerdTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems