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

DOI10.1007/BF00881900zbMath0783.68117OpenAlexW2076819871MaRDI QIDQ1311396

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

higher-order logicnatural deductionproof systemslogical frameworkstacticstacticals

Mathematics Subject Classification ID

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

Related Items

Program tactics and logic tactics, A metatheory of a mechanized object theory, A Survey of the Proof-Theoretic Foundations of Logic Programming, Tactics for hierarchical proof, A semantic framework for proof evidence, Forum: A multiple-conclusion specification logic, Representing proof transformations for program optimization, Tactic theorem proving with refinement-tree proofs and metavariables, A tactic calculus. --- Abridged version, The calculus of constructions as a framework for proof search with set variable instantiation, The practice of logical frameworks

Uses Software

• Prolog
• Nuprl
• Elf

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Depth-first iterative-deepening: An optimal admissible tree search
• The calculus of constructions
• Unification under a mixed prefix
• A unification algorithm for typed \(\overline\lambda\)-calculus
• The foundation of a generic theorem prover
• Uniform proofs as a foundation for logic programming
• Higher-order Horn clauses
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A framework for defining logics
• A formulation of the simple theory of types