Extracting Proofs from Tabled Proof Search

DOI10.1007/978-3-319-03545-1_13zbMath1426.68174OpenAlexW2245184119MaRDI QIDQ2938048

Alwen Tiu, Dale A. 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)

Related Items (2)

Extracting Proofs from Tabled Proof Search ⋮ A proof theory for model checking

Uses Software

• Bedwyr

Cites Work

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

This page was built for publication: Extracting Proofs from Tabled Proof Search