A semantic basis for proof queries and transformations

DOI10.1007/978-3-642-45221-5_4MaRDI QIDQ2870114zbMATH OpenOpenAlexFDO

Authors Ewen Denney, Christoph Lüth, D. Aspinall

Publication date 17 January 2014

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2060/20140005390

Mathematics Subject Classification ID

Recommendations

• Querying proofs
• Hiproofs: a hierarchical notion of proof tree
• A Tactic Language for Hiproofs
• Capturing hiproofs in HOL light
• Tactics for hierarchical proof

Cited in

(5)

• A semantic backward chaining proof system
• Hiproofs: a hierarchical notion of proof tree
• Querying proofs
• scientific article; zbMATH DE number 6819811 (Why is no real title available?)
• A general proof rule for procedures in predicate transformer semantics

Describes a project that uses

Uses Software

• XDuce

This page was built for publication: A semantic basis for proof queries and transformations

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