Automated Reasoning

Zusatztext

InhaltsangabeFrom 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.

Weitere Details