Soundness and completeness proofs by coinductive methods
From MaRDI portal
Publication:2362498
DOI10.1007/s10817-016-9391-3zbMath1409.68251OpenAlexW2534205211WikidataQ113901247 ScholiaQ113901247MaRDI QIDQ2362498
Dmitriy Traytel, Jasmin Christian Blanchette, Andrei Popescu
Publication date: 10 July 2017
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://eprints.mdx.ac.uk/21796/1/JAR2016.pdf
completenessfirst-order logiclazy evaluationsoundnesstableau systemsGentzen systemsIsabelle/HOLproof assistantscodatatypes
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (8)
Formalized soundness and completeness of epistemic logic ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formalization of the resolution calculus for first-order logic ⋮ A formalized general theory of syntax with bindings ⋮ Programming and verifying a declarative first-order prover in Isabelle/HOL ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Formalizing a Seligman-style tableau system for hybrid logic (short paper)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A certified, corecursive implementation of exact real numbers
- Higher-order rewrite systems and their confluence
- Isabelle/HOL. A proof assistant for higher-order logic
- Institution-independent model theory
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- Formalization of the Resolution Calculus for First-Order Logic
- Mechanizing the Metatheory of Sledgehammer
- The Gödel Completeness Theorem for Uncountable Languages
- Truly Modular (Co)datatypes for Isabelle/HOL
- Concrete Semantics
- Foundational extensible corecursion: a proof assistant perspective
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
- Sequent calculi for induction and infinite descent
- Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique
- Cyclic proofs of program termination in separation logic
- Unified Classical Logic Completeness
- A completeness theorem in modal logic
- Code Generation via Higher-Order Rewrite Systems
- An Institutional Version of Gödel’s Completeness Theorem
- Elements of Stream Calculus
- Automated Cyclic Entailment Proofs in Separation Logic
- Encoding Monomorphic and Polymorphic Types
- Theorem Proving in Higher Order Logics
- Automated Reasoning with Analytic Tableaux and Related Methods
- Equality of streams is a Π0 over 2-complete problem
- Typed Lambda Calculi and Applications
- An Effective Algorithm for the Membership Problem for Extended Regular Expressions
This page was built for publication: Soundness and completeness proofs by coinductive methods
