Extracting proofs from tabled proof search

DOI10.1007/978-3-319-03545-1_13MaRDI QIDQ2938048zbMATH OpenOpenAlexFDO

Authors Alwen Tiu, Dale Miller

Publication date 13 January 2015

Published in Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-00863561/file/root.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Beyond Bisimulation: The “up-to” Techniques
• Incorporating Tables into Proofs
• A coinductive approach to proof search
• Tabling, rational terms, and coinduction finally together!
• Coalgebraic bisimulation-up-to

Cites work

• Checking NFA equivalence with bisimulations up to congruence
• Coinductive Logic Programming
• Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
• Cut elimination for a logic with induction and co-induction
• Encoding transition systems in sequent calculus
• Enhancements of the bisimulation proof method
• Extracting proofs from tabled proof search
• Incorporating Tables into Proofs
• On global induction mechanisms in aμ-calculus with explicit approximations
• On the bisimulation proof method
• Programming with higher-order logic.
• Proof search specifications of bisimulation and modal logics for the \({\pi}\)-calculus
• Sequent calculi for induction and infinite descent

Cited in

(3)

• A proof theory for model checking
• Extracting proofs from tabled proof search
• Incorporating Tables into Proofs

Describes a project that uses

Uses Software

• Bedwyr

This page was built for publication: Extracting proofs from tabled proof search

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2938048)