Extracting Proofs from Tabled Proof Search
From MaRDI portal
Publication:2938048
DOI10.1007/978-3-319-03545-1_13zbMath1426.68174MaRDI QIDQ2938048
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
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
Uses Software
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