Nadathur, G. A higher-order logic as the basis for logic programming. Ph.D. Dissertation, University of Pennsylvania, May 1987.  @ NUS  Home/Search   Document Details and Download   Summary   Related Articles   Check

....quantification over properties of properties of individuals; and so forth. Higher order (or # order) logic allows all these quantifications. A formula is simply a term of type bool . The logic programming language #Prolog, though based on higher order logic, forbids quantification over bool [24]. So it is really first order logic extended with typed # expressions. The meta logic of Isabelle avoids quantification over bool to simplify the theory, but this restriction is not enforced. Quantification over propositions permits many di#erent formulations of higherorder logic. Absurdity (#) ....

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, University of Pennsylvania, 1987.

....f(a,b) means (f(a) b) Type variables permit ML style type inference so that variables need not be declared. The following meta connectives are polymorphic: # prop) # Type variables may not appear in theorems. Polymorphic theorems would complicate higher order unification [12]; a polymorphic higher order logic treads dangerously close to inconsistency [4] A typed object logic can be represented by making the object level typing rules explicit. See the section on Constructive Type Theory, which is the ultimate example of a typed logic. 2.2 The ml type term There are ....

G. Nadathur, A Higher-Order Logic as the Basis for Logic Programming, PhD Thesis, University of Pennsylvania (1987).

.... Declarative and Operational Over the past decade a series of papers have provided semantics for certain classical or intuitionistic fragments of HOHH (see [22, 3] based on work by Henkin [13] and Andrews [1] on the semantics of Church s classical Type theory [6] Nadathur s dissertation [20] provides a notion of term model for the HOHH fragment. Miller de nes a Kripke like bottom up semantics for a rst order fragment [15] in which the syntax of programs is built into the notion of model. In A semantics for Prolog , D.A. Wolfram [22] provided semantics for the classical higherorder ....

....syntax of programs is built into the notion of model. In A semantics for Prolog , D.A. Wolfram [22] provided semantics for the classical higherorder Horn clause fragment of Prolog, a result which was independently established in Bai and Blair [3] and was built on work in Nadathur s dissertation [20] and Andrews V complexes [2] However, the larger hereditarily Harrop fragment considered here requires intuitionistic logic and, consequently, an intuitionistic model theory. Until recently (see [8, 9] no such semantics had been developed even for the intuitionistic Church s type theory of ....

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, 1987.

....the structure of programs. The subscripted G means that 8 and ) can be used as constructors of goals 1 (clause bodies) Recall that bodies of Horn clauses admit only conjunction (i.e. G ) Possible applications of Prolog are chiefly the applications that motivated the introduction of terms [45, 40]: manipulation of formulas, computation of denotations, etc. see Section 4.1) Notice also that the structure of Prolog encompasses such constructions as modules [37] and abstract data types [35] without any extralogical addition. There have been actual applications of Prolog for automatic ....

....They often show how Prolog satisfies several requirements, but not a single and general requirement that justifies the whole of Prolog. At the beginning, Miller and Nadathur present a logic programming language called Prolog, which features higher order Horn clauses, terms, and equivalence [40, 45]. Then, Miller et al. 42, 41] introduce the connectives 8 G and )G , and keep the name Prolog. In several articles Miller 1 Similarly, a subscripted D means that a connective can be used as a constructor for definite clauses. For instance, Horn clauses are constructed with the implication ....

[Article contains additional citation context not shown here]

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD Thesis, University of Pennsylvania, 1987.

....instance, Horn clauses admit conjunctions in their bodies (i.e. G ) and Horn clauses are constructed with the implication connective (i.e. D , see more details on this in Section 2.1. 4) Possible applications of Prolog are chiefly the applications that motivated the introduction of terms [46, 40]: manipulation of formulas, computation of denotations, etc. see Section 3.1) Notice also that the structure of Prolog encompasses such constructions as modules [35] and abstract data types [33] without any extralogical additions. There have been actual applications of Prolog for automatic ....

....They often show how Prolog satisfies several requirements, but not a single and general requirement that justifies the whole of Prolog. In the beginning, Miller and Nadathur present a logic programming language called Prolog, which features higher order Horn clauses, terms, and equivalence [40, 46]. Then, Miller formalizes module importation as logical implication in goals, G [35] and module abstraction as universal quantification in goals, 8 G [33] Miller et al. observe that these extensions form a well behaved fragment of intuitionistic logic [43, 42] This fragment is called ....

[Article contains additional citation context not shown here]

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD Thesis, University of Pennsylvania, 1987.

....clause or program clauses, and a finite subset of P is a program. While this language is not, strictly speaking, first order, it is far from having the complex meta theory or theorem proving problems associated with higher order logics and logic programming languages (accounts of which are in [12, 14, 16]) As we shall show, a constrained form of first order unification makes it possible to implement complete theorem provers and interpreters for L. Simple modifications of the proof theory discussions in [9] show that P I G (where I denote intuitionistic provability) if and only if the sequent ....

....constants to appear within terms. Operationally speaking, we are making this extension 7. Encapsulation of state 14 May 1997 to allow goal formulas to be passed around as arguments and to be dynamically called. Various higher order extensions to logic programming have been analyzed in the papers [12, 14, 16]. The extension mentioned above is part of the much more general theory of higherorder hereditary Harrop formulas described in [14] Although there is not sufficient space here to present details, it suffices to say that when propositional variables are not permitted as the head of definite ....

G. Nadathur, A Higher-Order Logic as the Basis for Logic Programming, Ph.D. dissertation, University of Pennsylvania, May 1987.

.... may also be examined in terms of a formalization of semantic interpretation rules in a suitable higherorder logic, as has been done for inference rules of various logics by Felty and Miller [13, 14] using as rule metalanguage the higher order hereditary Harrop formulas [29] implemented in #Prolog [36, 37]. Rather than repeating here the precise definitions found elsewhere [13, 29, 36] the language will be introduced by showing how the typing rules of the previous section would be expressed [13] The #Prolog program in Figure 2 consists of certain declarations followed by two clauses. The ....

.... rules in a suitable higherorder logic, as has been done for inference rules of various logics by Felty and Miller [13, 14] using as rule metalanguage the higher order hereditary Harrop formulas [29] implemented in #Prolog [36, 37] Rather than repeating here the precise definitions found elsewhere [13, 29, 36], the language will be introduced by showing how the typing rules of the previous section would be expressed [13] The #Prolog program in Figure 2 consists of certain declarations followed by two clauses. The declarations specify expr and ty as the atomic types of (objectlevel) expressions and ....

[Article contains additional citation context not shown here]

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, University of Pennsylvania, 1986.

....fragment [8] in which the syntax of programs is built into the notion of model. In A semantics for Prolog , D.A. Wolfram [16] provided semantics for the higher order Horn clause fragment of Prolog, a result which was independently established in Bai and Blair [3] and was implicit in Nadathur [13]. These authors used Andrews V complexes [1] to provide a classical model theory for the higher order Horn clause fragment of Prolog. However, the larger hereditarily Harrop fragment requires constructive logic and a constructive model theory. Operationality: bottom up semantics In [8] Miller ....

....ae( x:G) c) i; B where c is a fresh constant of label i 1. 5 Models for Prolog In A semantics for Prolog , D.A. Wolfram [16] provided semantics for the higher order Horn clause fragment of Prolog, a result which was independently established in Bai and Blair [3] and was implicit in Nadathur [13]. These authors used Andrews V complexes [1] to provide a classical model theory for the higher order Horn clause fragment of Prolog. However, the larger hereditarily Harrop fragment requires constructive logic and a constructive model theory. Although models for the lambda calculus sound for j ....

Gopalan Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, 1987.

.... Semantics: Declarative and Operational Over the past decade a series of papers have provided semantics for certain classical or intuitionistic fragments of HOHH (see [16, 3] based on work by Henkin [6] and Andrews [1] on the semantics of Church s classical Type theory [4] Nadathur s dissertation [12] provides a notion of term model for the HOHH fragment and lays ground work for a bottom up semantics. Miller defined a Kripke like bottom up semantics for a first order fragment [8] in which the syntax of programs is built into the notion of model. In A semantics for Prolog , D.A. Wolfram [16] ....

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, 1997.

....extension of Horn clauses which does support embedded implications. This larger logical fragment was proved to preserve the proof theoretic properties at the basis of the logic paradigm, namely to be a uniform proof system [14] Higher order Hereditary Harrop formulas underlie the languages Prolog[15] and Isabelle [18] first order Hereditary Harrop formulas are explored in [9, 10] In addition to embedded implications, Hereditary Harrop formulas allow universal quantifications in the bodies of clauses. The combination of these two extensions provides a rich notion of dynamic scoping, which ....

Gopalan Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, University of Pennsylvania, 1987.

....issues are a good guide for implementing logic programming systems. Speed was always our second concern. We assume a knowledge of Prolog and Prolog, their semantics, and their basic algorithms: logical variable, search stack, unification, unification [18] deduction rules, and uniform proofs [32, 30]. We adopt an architectural presentation: in section 3, we present the kernel subsystem that is in charge of the elementary representation problems, in section 4, we present a software layer which is both a specialisation and an extension of the kernel, finally, in section 5, we present the ....

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. Ph.D. Thesis, University of Pennsylvania, 1987.

.... 1 1 Introduction In the context of logic programming languages, several attempts have been made to realize higher order extensions to this paradigm and especially two natural approaches have been proposed: the higher order logic approach , as for example it has been investigated in [Nadathur 87, Chen 89, Wadge 91] and the metalogical approach (as for example it has been studied in [Burt 90, Costantini 89, Warren 82] In this work we analyze parallel implementation issues of higher order features in logic programming, following the higherorder logic approach, and starting in ....

....of as a procedure that, given a program P , attempts to construct a P derivation for goal formulas. A state in this derivation process is characterized by a set of goals and a disagreement set, and the search for a solution is progressed by applying a simple step to one of these components. In [Nadathur 87] it is shown that this derivation process is complete, and that the order in which rules are applied in correspondence of the choice points does not affect the final result. As a consequence, non determinism can be exploited to extract some parallelism, provided that the resulting process can be ....

[Article contains additional citation context not shown here]

G. Nadathur, A higher-order logic as the basis for logic programming, Ph.D Dissertation, University of Pennsylvania, May 1987.

....issues are a good guide for implementing logic programming systems. Speed was always our second concern. We assume a knowledge of Prolog and Prolog, their semantics, and their basic algorithms: logical variable, search stack, unification, unification [20] deduction rules, and uniform proofs [34, 32]. We adopt an architectural presentation: in section 2, we present the kernel subsystem that is in charge of the elementary representation problems, in section 3, we present a software layer which is both a specialization and an extension of the kernel, finally, in section 4, we present the ....

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. Ph.D. Thesis, University of Pennsylvania, 1987.

.... type variables) and the procedure given there has been incorporated into the generic theorem prover Isabelle [Pau90] Elliott ( Ell89] presents an algorithm for unification in the presence of dependent function types, designed as the basis for a generalization of the programming language Prolog [Nad87]. Each of these algorithms is based on Huet s method; neither of them is a complete unification procedure. Higher order unification is undecidable [Hue73] even when restricted to second order terms [Gol81] The first complete enumeration methods for higher order unification are due to ....

G. Nadathur. A higher-order logic as the basis for logic programming. Dissertation, University of Pennsylvania, 1987.

....exist when unifiers do exist. Prolog addresses these issues by implementing a depth first version of the unification search procedure described by Huet [24] It was shown by Miller et al. 30] that such unification is sufficient for determining substitutions, and by Nadathur and Miller [31, 33], that this unification procedure can be smoothly integrated into the usual backtracking mechanism of logic programming languages. The higher order unification problems we shall encounter in this paper are all rather simple. In fact all such problems are decidable. The presence of logic variables ....

Gopalan Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, University of Pennsylvania, Technical Report MS-CIS-87-48, June 1987.

....and projection. The preconditions of the two rules are not exclusive, hence the non determinism. This search procedure calls for some remarks. 1. A pair X; t (X does not occur in t) has a most general unifier X t which is computed expensively by MATCH. SIMPL calls a procedure, named TRIV in [7], that handles cheaply as many as possible similar cases. 2. A flexible flexible pair is not solved but delayed as a constraint. The constraint will be tested for satisfiability as soon as the pair becomes more rigid. 3. Types are essential because (1) in a non typed calculus some terms have no ....

....An occurrence of X in t may be discarded by further reduction. Sufficient criteria for performing the trivial unifications are presented by Huet. A failure of TRIV does not imply a failure of unification. It only means that the general procedure must be applied. The permutation version of TRIV[7] is not implemented in the measured system, but it can be, and probably will be in a near future. As for first order Prolog, the occurrence check is not implemented. j expansion causes an unknown X to be replaced by u Delta (X u) An efficient TRIV procedure must recognise similar cases. When ....

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. Ph.D. Thesis, University of Pennsylvania, 1987.

.... in clause heads must be the same (i.e. they are not independent instances) The head condition is implicit in the Mycroft O Keefe discipline [17] It is explicitly enforced in the Godel system [10] and in our implementation of Prolog [2] It is not mentioned in the first writings on Prolog [14, 18], but it is rejected in further works [19] An objective of this article is to give support to enforcing the head condition. The head condition makes the inference of the types of predicate constants non decidable, but this will not be a problem here since we assume that all constants have their ....

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. Ph.D. Thesis, University of Pennsylvania, 1987.

....the realization that a subset of first order predicate logic, namely definite clauses, can be given a procedural interpretation. It is well known that the paradigm of pure definite clauses has serious limitations as a programming language, and this has prompted variations of this basic framework [21, 30]. An important development in this vein is the paradigm of constraint logic programming (CLP) 17, 18] Essentially, a CLP scheme is parameterized by a domain, such as reals, and certain function symbols ( Gamma, etc. and predicates ( etc. have pre defined meanings. Computationally, the ....

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, University of Pennsylvania, 1987.

....to consider Forum as a proof theoretical foundation of linear logic programming. In this sense it is interesting to study suitable subclasses of formulas which can help in fixing a programming methodology for the logic, as Horn Clauses (Prolog [41] for CL and hereditary Harrop formulas (Prolog [37]) for Intuitionistic Logic. In our work [14] we have tried to isolate a particular subset of Forum enjoying the good properties that the subset of higher order hereditary Harrop formulas does [36] We called the considered class of formulas E hhf , standing for extended hereditary Harrop ....

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming, MS-CIS-87-48, LINC LAB 69. Technical report, Dept. of Computer and Information Science, School of Engineering and Applied Science, University of Pennsylvania, Philadelphia, 1987.

....We propose a novel logic, called HiLog, which provides a clean declarative semantics to much of this higher order logic programming. From the outset, even the terminology of higher orderness seems ill defined. A number of works have proposed various higher order constructs in the logic framework [1, 5, 13, 7, 23, 24, 30, 31, 42, 45] but with such a diversity of syntax and semantics, it is not always clear what kind of higher orderness is being claimed. In our opinion, there are at least two different facets to the issue: a higher order This paper is an expanded version of the work previously reported in [10, 11] y ....

....say p and q, to be interpreted by the same relation and yet the equality p = q be false. The above examples represent the two extreme cases, in a sense. There are higher order languages with a first order semantics that embody a non trivial equality theory. An example is a subset of Prolog [42, 45] that has no type variables and whose syntax is essentially the same as Church s simple theory of types [13] Equality in Prolog corresponds to equivalence and is not extensional: there may exist predicates that are not equivalent but still extensionally equal. To better see the role of ....

[Article contains additional citation context not shown here]

Nadathur, G. [1987] A Higher-Order Logic as the Basis for Logic Programming, Ph.D. Dissertation, University of Pennsylvania, June 1987.

No context found.

Nadathur, G. A higher-order logic as the basis for logic programming. Ph.D. Dissertation, University of Pennsylvania, May 1987.

....this paper provides for a language with such an enrichment and consequently leads to a language that potentially has several novel applications. Detailed experiments in some of the application realms show that this potential is in fact borne out. The interested reader may refer, for instance, to [7, 13, 20, 22, 25, 29] for the results of these experiments. It should be mentioned that the extension to first order Horn clauses described in this paper is not the only one possible that preserves the spirit of properties (i) iv) The primary aim here is that of examining the nature and role of higher order ....

....unification [15] with backchaining and goal reductions and constitutes a higher order generalization to SLD resolution. These results have been used to describe a logic programming language called Prolog. A presentation of this language is beyond the scope of this paper but may be found in [21, 25, 27]. 2. A Higher Order Logic The higher order logic used in this paper is derived from Church s formulation of the simple theory of types [5] principally by the exclusion of the axioms concerning infinity, choice, extensionality and description. Church s logic is particularly suited to our purposes ....

[Article contains additional citation context not shown here]

Nadathur, G. A higher-order logic as the basis for logic programming. Ph.D. Dissertation, University of Pennsylvania, May 1987.

....a brief exposition to this language, since we shall need it in the discussions in the rest of this paper. This exposition is deliberately brief since the theoretical issues pertaining to this language are not of importance in the present context, and have been the object of our study elsewhere [9, 10]. While Prolog contains features such as predicate variables, for the purposes of this paper we ignore these and view this language as one that extends Prolog by replacing firstorder terms with typed terms in which function variables may appear. Typed terms are essentially those terms that can ....

G. Nadathur, "A Higher-Order Logic as the Basis for Logic Programming," Ph.D. Dissertation, University of Pennsylvania, May 1987.

....Prolog [20] has, over the last five years, been a testbed for experimenting with several different extensions to a language such as Prolog. The initial impetus in developing this language was provided by a desire to understand the nature and role of higher order notions within logic programming [12, 19, 21]. This goal was subsequently expanded to include devices for other forms of abstraction such as lexical scoping, modules and abstract data types [9, 10, 13] The purpose of this paper is to discuss another important but somewhat less exposed component of the language, namely its type system. The ....

....of utilizing intensional occurrences of predicate variables in finding meaningful substitutions for them that then give rise to complex computations by virtue of extensional occurrences of the same predicate variables. A more detailed discussion of such uses of predicate variables may be found in [19]. 2.3 Type Variables A closer look at the declarations encountered so far reveals that the use of simple types makes the definitions of procedures more specific than they need to be. Thus, the predicates member , mapfun and mappred as defined above pertain only to lists of integers even though ....

[Article contains additional citation context not shown here]

Nadathur, G. A higher-order logic as the basis for logic programming. Ph.D. Dissertation, University of Pennsylvania, May 1987.

No context found.

G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, University of Pennsylvania, 1987.

First 50 documents

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.