Soundness and completeness proofs by coinductive methods

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

zbMATH Keywords

completenessfirst-order logiclazy evaluationsoundnesstableau systemsGentzen systemsIsabelle/HOLproof assistantscodatatypes

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03)

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

• ML
• Isabelle/HOL
• HOL
• Sledgehammer
• Cyclist
• Completeness theorem
• Abstract Completeness
• FOL Fitting
• Archive Formal Proofs

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