A Proof-Theoretic Approach to Tactics

DOI10.1007/11812289_6MaRDI QIDQ5756755zbMATH OpenOpenAlexFDO

Authors Kamal Aboul-Hosn

Publication date 5 September 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11812289_6

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Tactics and parameters
• A tactic calculus. --- Abridged version
• Tactics and certificates in Meta Dedukti
• Reflection of formal tactics in a deductive reflection framework
• PVS\#: streamlined tacticals for PVS

Cited in

(22)

• Program tactics and logic tactics
• There are more strategy-proof procedures than you think
• Tactics and certificates in Meta Dedukti
• A tactic calculus. --- Abridged version
• Writing programs that construct proofs
• scientific article; zbMATH DE number 1670747 (Why is no real title available?)
• A pragmatic approach to reuse in tactical theorem proving
• A calculus of tactics and its operational semantics
• Tinycals: step by step tacticals
• Implicational rewriting tactics in HOL
• Standalone Tactics Using OpenTheory
• scientific article; zbMATH DE number 2177623 (Why is no real title available?)
• scientific article; zbMATH DE number 3870643 (Why is no real title available?)
• scientific article; zbMATH DE number 1104384 (Why is no real title available?)
• Reflection of formal tactics in a deductive reflection framework
• Tactics and parameters
• Refactoring proofs with Tactician
• Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
• Theorem Proving in Higher Order Logics
• A Tactic Language for Hiproofs
• Tactics for hierarchical proof
• Using probabilistic Kleene algebra pKA for protocol verification

This page was built for publication: A Proof-Theoretic Approach to Tactics

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