scientific article; zbMATH DE number 3870643

MaRDI QIDQ3336739zbMATH OpenFDO

Authors David A. Schmidt

Publication date 1984

zbMATH Keywords

LCFtactical theorem provingcontrol algorithms of natural deduction theorem proversLogic for Computable Functionsproof discovery algorithms

Mathematics Subject Classification ID

Recommendations

• Implementing tactics and tacticals in a higher-order logic programming language
• A calculus of tactics and its operational semantics
• Program tactics and logic tactics
• A Proof-Theoretic Approach to Tactics
• Theorem Proving in Higher Order Logics
• Strategic computation and deduction
• Strategy representation and reasoning in the situation calculus
• A logic for rewriting strategies
• A Tactic Language for Hiproofs

Cited in

(3)

• A generalized operator notation and its properties
• A tactic calculus. --- Abridged version
• A calculus of tactics and its operational semantics

This page was built for publication:

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