Loading...
Please wait, while we are loading the content...
Similar Documents
Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language (1993)
| Content Provider | CiteSeerX |
|---|---|
| Author | Felty, Amy |
| Abstract | 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 -terms, replacing first-order unification with higher-order unification, and allowing implication and universal quantification in queries and the bodies of clauses. Inference rules for a variety of inference systems can be naturally specified in this language. The higher-order features of the language contribute to a concise specification of provisos concerning variable occurrences in formulas and the discharge of assumptions present in many inference systems. Tactics and tacticals, which provide a framework for high-level control over search for proofs, can be directly and naturally implemented in the extended language. This framework serves as a starting point for implementing theorem provers an... |
| File Format | |
| Volume Number | 11 |
| Journal | Journal of Automated Reasoning |
| Language | English |
| Publisher Date | 1993-01-01 |
| Access Restriction | Open |
| Subject Keyword | Higher-order Logic Programming Language Theorem Provers Inference Rule Higher-order Intuitionistic Logic Higher-order Unification Universal Quantification Higher-order Feature Simply-typed Term Many Inference System Traditional Logic Programming Language Logic Programming Language Starting Point Tactic Style Theorem Provers Concise Specification High-level Control Extended Language First-order Unification First-order Term Variable Occurrence Language Contribute Inference System |
| Content Type | Text |
| Resource Type | Article |
