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 / [electronic resource] :
edited by Stéphane Demri, Deepak Kapur, Christoph Weidenbach.
- Cham : Springer International Publishing, 2014.
- 1 online resource (XXVIII, 528 p. 101 ill.)
- Lecture Notes in Computer Science, 8562 0302-9743 ; .
From Reachability to Temporal Specifications in Cost-Sharing Games -- Electronic Voting: How Logic Can Help -- And-Or Tableaux for Fix point Logics with Converse: LTL, CTL, PDL and CPDL -- Unified Classical Logic Completeness: A Coinductive Pearl -- A Focused Sequent Calculus for Higher-Order Logic -- SAT-Based Decision Procedure for Analytic Pure Sequent Calculi -- A Unified Proof System for QBF Pre processing -- The Fractal Dimension of SAT Formulas -- A Gentle Non-disjoint Combination of Satisfiability Procedures -- A Rewriting Strategy to Generate Prime Implicates in Equational Logic -- Finite Quantification in Hierarchic Theorem Proving -- Computing All Implied Equalities via SMT-Based Partition Refinement -- Proving Termination of Programs Automatically with A Pro VE -- Locality Transfer: From Constrained Axiomatizations to Reachability Predicates -- Proving Termination and Memory Safety for Programs with Pointer Arithmetic -- QBF Encoding of Temporal Properties and QBF-Based Verification -- Introducing Quantified Cuts in Logic with Equality -- Quati: An Automated Tool for Proving Permutation Lemmas -- A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description -- M lean CoP: A Connection Prover for First-Order Modal Logic -- Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+ -- dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems -- Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications -- Clausal Resolution for Modal Logics of Confluence -- Implementing Tableau Calculi Using BDDs: BDDTab System Description -- Approximations for Model Construction -- A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic -- StarExec: A Cross-Community Infrastructure for Logic -- Skeptik: A Proof Compression System -- Terminating Minimal Model Generation Procedures for Propositional Modal Logics -- Cool - A Generic Reasoner for Coalgebraic Hybrid Logics (System Description) -- The Complexity of Theorem Proving in Circumscription and Minimal Entailment -- Visibly Linear Temporal Logic -- Count and Forget: Uniform Interpolation of SHQ- Ontologies -- Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures -- EL-ifying Ontologies -- The Bayesian Description Logic BEL -- OTTER Proofs in Tarskian Geometry -- NESCOND: An Implementation of Nested Sequent Calculi for Conditional Logics -- Knowledge Engineering for Large Ontologies with Sigma KEE 3.0.