Patrick Nicodemus (May 12 2023 at 19:51): Patrick Nicodemus (May 12 2023 at 19:51):Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language
We argue that a logic programming language with a higher-order intuitionistic logic as its foundation can be used both to naturally specify and implement tactic style theorem provers. The language extends traditional logic programming languages by replacing first-order terms with simply-typed lambda terms, replacing first-order quantification with higher-order quantification, and allowing implication and universal quantification in queries and the bodies of clauses.
https://www.site.uottawa.ca/~afelty/dist/jar93.pdf
Last updated: Oct 13 2024 at 01:02 UTC