In this paper we present a mechanism to define names for proof-wit nesses of formulae and thus to use Gent zen’s cut-rule in logic programming. We consider a program to be a set of logical formulae together with a list of such definitions. Occurrences of the defined names guide the proof-search by indicating when an instance of the cut-rule should be attempted. By using the cut-rule there are proofs that can be made dramatically shorter. We explain how this idea of using the cut-rule can be applied to the logic of hereditary Harrop formulae.
CITATION STYLE
Pinto, L. (1994). Cut formulae and logic programming. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 798 LNAI, pp. 282–300). Springer Verlag. https://doi.org/10.1007/3-540-58025-5_62
Mendeley helps you to discover research relevant for your work.