Automated Reasoning with Analytic Tableaux and Related Methods
From MaRDI portal
Publication:5479270
DOI10.1007/11554554zbMath1142.03366OpenAlexW2486590071MaRDI QIDQ5479270
Publication date: 7 July 2006
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11554554
Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Inductive definability (03D70)
Related Items (28)
Soundness and completeness proofs by coinductive methods ⋮ Soundness Conditions for Big-Step Semantics ⋮ Transforming orthogonal inductive definition sets into confluent term rewrite systems ⋮ Uniform interpolation from cyclic proofs: the case of modal mu-calculus ⋮ Cut-Elimination and Proof Schemata ⋮ Unnamed Item ⋮ Loop verification with invariants and contracts ⋮ On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs ⋮ Unnamed Item ⋮ Schematic refutations of formula schemata ⋮ Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting ⋮ A logical framework with higher-order rational (circular) terms ⋮ An efficient cyclic entailment procedure in a fragment of separation logic ⋮ Automated temporal verification for algebraic effects ⋮ Unnamed Item ⋮ Cyclic Arithmetic Is Equivalent to Peano Arithmetic ⋮ Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System ⋮ Unnamed Item ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ A synchronous effects logic for temporal verification of pure Esterel ⋮ Unnamed Item ⋮ Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs ⋮ Combining induction and saturation-based theorem proving ⋮ Schematic Cut Elimination and the Ordered Pigeonhole Principle ⋮ Non-well-founded deduction for induction and coinduction ⋮ Initial Algebra Semantics for Cyclic Sharing Structures ⋮ Induction and Skolemization in saturation theorem proving ⋮ Loop-check specification for a sequent calculus of temporal logic
This page was built for publication: Automated Reasoning with Analytic Tableaux and Related Methods
