default search action
7th IJCAR 2014: Vienna, Austria
- Stéphane Demri, Deepak Kapur, Christoph Weidenbach:
Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings. Lecture Notes in Computer Science 8562, Springer 2014, ISBN 978-3-319-08586-9
Invited Papers
- Guy Avni, Orna Kupferman, Tami Tamir:
From Reachability to Temporal Specifications in Cost-Sharing Games. 1-15 - Véronique Cortier:
Electronic Voting: How Logic Can Help. 16-25 - Rajeev Goré:
And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL. 26-45
HOL
- Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
:
Unified Classical Logic Completeness - A Coinductive Pearl. 46-60 - Fredrik Lindblad:
A Focused Sequent Calculus for Higher-Order Logic. 61-75
SAT and QBF
- Ori Lahav
SAT-Based Decision Procedure for Analytic Pure Sequent Calculi. 76-90 - Marijn Heule, Martina Seidl, Armin Biere
A Unified Proof System for QBF Preprocessing. 91-106 - Carlos Ansótegui
The Fractal Dimension of SAT Formulas. 107-121
SMT
- Paula Daniela Chocron
A Gentle Non-disjoint Combination of Satisfiability Procedures. 122-136
Equational Reasoning
- Mnacho Echenim, Nicolas Peltier, Sophie Tourret:
A Rewriting Strategy to Generate Prime Implicates in Equational Logic. 137-151 - Peter Baumgartner, Joshua Bax, Uwe Waldmann:
Finite Quantification in Hierarchic Theorem Proving. 152-167 - Josh Berdine, Nikolaj S. Bjørner:
Computing All Implied Equalities via SMT-Based Partition Refinement. 168-183 - Jürgen Giesl
Proving Termination of Programs Automatically with AProVE. 184-191
Verification
- Matthias Horbach, Viorica Sofronie-Stokkermans:
Locality Transfer: From Constrained Axiomatizations to Reachability Predicates. 192-207 - Thomas Ströder, Jürgen Giesl
Proving Termination and Memory Safety for Programs with Pointer Arithmetic. 208-223 - Wenhui Zhang:
QBF Encoding of Temporal Properties and QBF-Based Verification. 224-239
Proof Theory
- Stefan Hetzl
Introducing Quantified Cuts in Logic with Equality. 240-254 - Vivek Nigam, Giselle Reis, Leonardo Lima
Quati: An Automated Tool for Proving Permutation Lemmas. 255-261 - Rajeev Goré, Jimmy Thomson, Jesse Wu:
A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description. 262-268 - Jens Otten
MleanCoP: A Connection Prover for First-Order Modal Logic. 269-276
Modal and Temporal Reasoning
- Serenella Cerrito, Amélie David, Valentin Goranko:
Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+. 277-291 - Jean-Baptiste Jeannin, André Platzer
dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems. 292-306 - Björn Lellmann
Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications. 307-321 - Cláudia Nalon, João Marcos
Clausal Resolution for Modal Logics of Confluence. 322-336 - Rajeev Goré, Kerry Olesen, Jimmy Thomson:
Implementing Tableau Calculi Using BDDs: BDDTab System Description. 337-343
SMT and SAT
- Aleksandar Zeljic, Christoph M. Wintersteiger
Approximations for Model Construction. 344-359 - Rüdiger Ehlers
A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic. 360-366 - Aaron Stump, Geoff Sutcliffe
StarExec: A Cross-Community Infrastructure for Logic Solving. 367-373 - Joseph Boudou, Andreas Fellner, Bruno Woltzenlogel Paleo:
Skeptik: A Proof Compression System. 374-380
Modal Logic
- Fabio Papacchini, Renate A. Schmidt
Terminating Minimal Model Generation Procedures for Propositional Modal Logics. 381-395 - Daniel Gorín, Dirk Pattinson, Lutz Schröder
Cool - A Generic Reasoner for Coalgebraic Hybrid Logics (System Description). 396-402
Complexity
- Olaf Beyersdorff
The Complexity of Theorem Proving in Circumscription and Minimal Entailment. 403-417 - Laura Bozzelli, César Sánchez
Visibly Linear Temporal Logic. 418-433
Description Logics
- Patrick Koopmann
Count and Forget: Uniform Interpolation of $\mathcal{SHQ}$ -Ontologies. 434-448 - Andreas Steigmiller, Birte Glimm, Thorsten Liebig:
Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures. 449-463 - David Carral, Cristina Feier
EL-ifying Ontologies. 464-479
Knowledge Representation and Reasoning
- Ismail Ilkan Ceylan, Rafael Peñaloza
The Bayesian Description Logic ${\mathcal{BEL}}$. 480-494 - Michael Beeson, Larry Wos:
OTTER Proofs in Tarskian Geometry. 495-510 - Nicola Olivetti, Gian Luca Pozzato:
NESCOND: An Implementation of Nested Sequent Calculi for Conditional Logics. 511-518 - Adam Pease, Stephan Schulz:
Knowledge Engineering for Large Ontologies with Sigma KEE 3.0. 519-525
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-18 18:34 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: