Implementing tactics and tacticals in a higher-order logic programming language

DOI10.1007/BF00881900MaRDI QIDQ1311396zbMATH OpenOpenAlexFDO

Authors Amy P. Felty

Publication date 23 January 1994

Published in Journal of Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

natural deductionhigher-order logiclogical frameworksproof systemstacticstacticals

Mathematics Subject Classification ID

Artificial intelligence (68T99) Logic programming (68N17)

Recommendations

• scientific article; zbMATH DE number 4053062
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 1670747
• Programming with higher-order logic.
• A treatment of higher-order features in logic programming

Cites work

• scientific article; zbMATH DE number 3978351 (Why is no real title available?)
• scientific article; zbMATH DE number 4053062 (Why is no real title available?)
• scientific article; zbMATH DE number 65531 (Why is no real title available?)
• scientific article; zbMATH DE number 65533 (Why is no real title available?)
• scientific article; zbMATH DE number 516994 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A formulation of the simple theory of types
• A framework for defining logics
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Depth-first iterative-deepening: An optimal admissible tree search
• Higher-order Horn clauses
• The calculus of constructions
• The foundation of a generic theorem prover
• Unification under a mixed prefix
• Uniform proofs as a foundation for logic programming

Cited in

(17)

• Tactics for hierarchical proof
• Tactic theorem proving with refinement-tree proofs and metavariables
• The practice of logical frameworks
• Program tactics and logic tactics
• A tactic calculus. --- Abridged version
• scientific article; zbMATH DE number 1670747 (Why is no real title available?)
• The calculus of constructions as a framework for proof search with set variable instantiation
• Representing proof transformations for program optimization
• A Survey of the Proof-Theoretic Foundations of Logic Programming
• A calculus of tactics and its operational semantics
• Higher-order annotated terms for proof search
• Forum: A multiple-conclusion specification logic
• A metatheory of a mechanized object theory
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 3870643 (Why is no real title available?)
• A semantic framework for proof evidence
• scientific article; zbMATH DE number 4053062 (Why is no real title available?)

Describes a project that uses

Uses Software

• Prolog
• Nuprl
• Elf

This page was built for publication: Implementing tactics and tacticals in a higher-order logic programming language

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