Implementing tactics and tacticals in a higher-order logic programming language
From MaRDI portal
Publication:1311396
DOI10.1007/BF00881900zbMath0783.68117OpenAlexW2076819871MaRDI QIDQ1311396
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
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
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