Reflection of formal tactics in a deductive reflection framework

DOI10.1007/3-540-61511-3_118zbMath1412.68257OpenAlexW1540592429MaRDI QIDQ4647552

Harald Ruess

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

proof termreflection principledecision procedurecorrectness criterionabstract syntax

Mathematics Subject Classification ID

Uses Software

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

Cites Work

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

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