Extracting Proofs from Tabled Proof Search

DOI10.1007/978-3-319-03545-1_13zbMath1426.68174MaRDI 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

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Related Items

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

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