Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

A proof procedure for the logic of hereditary Harrop formulas

A proof procedure for the logic of hereditary Harrop formulas A proof procedure is presented for a class of formulas in intuitionistic logic. These formulas are the so-calledgoal formulas in the theory of hereditary Harrop formulas. Proof search in intuitionistic logic is complicated by the nonexistence of a Herbrand-like theorem for this logic: formulas cannot in general be preprocessed into a form such as the clausal form, and the construction of a proof is often sensitive to the order in which the connectives and quantifiers are analyzed. An interesting aspect of the formulas we consider here is that this analysis can be carried out in a relatively controlled manner in their context. In particular, the task of finding a proof can be reduced to one of demonstrating that a formula follows from a set of assumptions, with the next step in this process being determined by the structure of the conclusion formula. An acceptable implementation of this observation must utilize unification. However, since our formulas may contain universal and existential quantifiers in mixed order, care must be exercised to ensure the correctness of unification. One way of realizing this requirement involves labelling constants and variables and then using these labels to constrain unification. This form of unification is presented and used in a proof procedure for goal formulas in a first-order version of hereditary Harrop formulas. Modifications to this procedure for the relevant formulas in a higher-order logic are also described. The proof procedure that we present has a practical value in that it provides the basis for an implementation of the logic programming language λProlog. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of Automated Reasoning Springer Journals

A proof procedure for the logic of hereditary Harrop formulas

Journal of Automated Reasoning , Volume 11 (1) – Dec 10, 2004

Loading next page...
 
/lp/springer-journals/a-proof-procedure-for-the-logic-of-hereditary-harrop-formulas-FKsnFYicVC

References (29)

Publisher
Springer Journals
Copyright
Copyright
Subject
Computer Science; Mathematical Logic and Formal Languages; Artificial Intelligence; Mathematical Logic and Foundations; Symbolic and Algebraic Manipulation
ISSN
0168-7433
eISSN
1573-0670
DOI
10.1007/BF00881902
Publisher site
See Article on Publisher Site

Abstract

A proof procedure is presented for a class of formulas in intuitionistic logic. These formulas are the so-calledgoal formulas in the theory of hereditary Harrop formulas. Proof search in intuitionistic logic is complicated by the nonexistence of a Herbrand-like theorem for this logic: formulas cannot in general be preprocessed into a form such as the clausal form, and the construction of a proof is often sensitive to the order in which the connectives and quantifiers are analyzed. An interesting aspect of the formulas we consider here is that this analysis can be carried out in a relatively controlled manner in their context. In particular, the task of finding a proof can be reduced to one of demonstrating that a formula follows from a set of assumptions, with the next step in this process being determined by the structure of the conclusion formula. An acceptable implementation of this observation must utilize unification. However, since our formulas may contain universal and existential quantifiers in mixed order, care must be exercised to ensure the correctness of unification. One way of realizing this requirement involves labelling constants and variables and then using these labels to constrain unification. This form of unification is presented and used in a proof procedure for goal formulas in a first-order version of hereditary Harrop formulas. Modifications to this procedure for the relevant formulas in a higher-order logic are also described. The proof procedure that we present has a practical value in that it provides the basis for an implementation of the logic programming language λProlog.

Journal

Journal of Automated ReasoningSpringer Journals

Published: Dec 10, 2004

There are no references for this article.