Reflection of formal tactics in a deductive reflection framework

DOI10.1007/3-540-61511-3_118zbMATH Open1412.68257OpenAlexW1540592429MaRDI QIDQ4647552FDOQ4647552

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

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

zbMATH Keywords

decision procedurereflection principlecorrectness criterionabstract syntaxproof term

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Title not available (Why is that?)
• Edinburgh LCF. A mechanized logic of computation
• Logic and Computation
• Title not available (Why is that?)
• Title not available (Why is that?)
• A framework for defining logics
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The calculus of constructions
• Self-reference and modal logic
• Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Prolegomena to a theory of mechanized formal reasoning
• Categorical abstract machines for higher-order typed \(\lambda\)-calculi
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

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

Uses Software

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

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)