Reflection of formal tactics in a deductive reflection framework

DOI10.1007/3-540-61511-3_118MaRDI QIDQ4647552zbMATH OpenOpenAlexFDO

Authors Harald Rueß

Publication date 15 January 2019

Published in Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61511-3_118

zbMATH Keywords

decision procedurereflection principlecorrectness criterionabstract syntaxproof term

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• A Proof-Theoretic Approach to Tactics
• Tactics and certificates in Meta Dedukti
• Extensible and efficient automation through reflective tactics
• Theorem Proving in Higher Order Logics
• Metalogical frameworks. II: Developing a reflected decision procedure

Cites work

• scientific article; zbMATH DE number 432706 (Why is no real title available?)
• scientific article; zbMATH DE number 3748393 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3596224 (Why is no real title available?)
• scientific article; zbMATH DE number 1331927 (Why is no real title available?)
• scientific article; zbMATH DE number 1006087 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A framework for defining logics
• Categorical abstract machines for higher-order typed -calculi
• Edinburgh LCF. A mechanized logic of computation
• Logic and Computation
• Prolegomena to a theory of mechanized formal reasoning
• Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
• Self-reference and modal logic
• The calculus of constructions
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(5)

• Theorem Proving in Higher Order Logics
• Algebraic Methodology and Software Technology
• Tactics and certificates in Meta Dedukti
• A Proof-Theoretic Approach to Tactics
• Practical reflection for sequent logics

Describes a project that uses

Uses Software

• Cambridge LCF
• LCF
• Nuprl
• HOL
• PVS
• ML
• Isabelle

This page was built for publication: Reflection of formal tactics in a deductive reflection framework

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