Tactic theorem proving with refinement-tree proofs and metavariables

DOI10.1007/3-540-58156-1_44zbMath1433.68546OpenAlexW1515228883MaRDI QIDQ5210800

Douglas J. Howe, Amy P. Felty

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_44

Mathematics Subject Classification ID

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

Related Items

KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems, Ornaments for Proof Reuse in Coq, The practice of logical frameworks

Uses Software

• Coq
• Nuprl
• LCF

Cites Work

• Implementing tactics and tacticals in a higher-order logic programming language
• Edinburgh LCF. A mechanized logic of computation
• Uniform proofs as a foundation for logic programming
• A Deductive Approach to Program Synthesis
• A framework for defining logics