### Higher-Order Logic Programming (1986)Higher-Order Logic Programming (1986)

Access Restriction
Open

 Author Nadathur, Gopalan ♦ Miller, Dale Source CiteSeerX Content type Text Publisher Academic Press File Format PDF Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science Subject Keyword Higher-order Logic Programming ♦ Propositional Horn Clause ♦ Tactic-style Encoding ♦ Definite Clause ♦ Cl4tac Truegoal ♦ Atomic Proposition ♦ Primitive Object-level Goal ♦ Proof Procedure ♦ Goal G2 ♦ Type Cl1tac ♦ Goal G1 ♦ Proposi51 Type ♦ Type Cl3tac ♦ Type Cl2tac ♦ Type Cl4tac ♦ Primitive Tactic ♦ G1 G2 Description ly, if a tactic R holds of G1 and G2, i.e., if (R G1 G2) is solvable from a presentation of primitive tactics as a set of definite clauses, then satisfying the goal G2 in the object-language should suffice to satisfy goal G1. An illustration of these ideas can be provided by considering the task of implementing a proof procedure for propositional Horn clauses. For simplicity of presentation, we restrict the proposi51 type p g. type q g. type r g. type s g. type cl1tac g -? g -? o. type cl2tac g -? g -? o. type cl3tac g -? g -? o. type cl4tac g -? g -? o. (cl1tac p (andgoal r s)). (cl2tac q r). (cl3tac s (andgoal r q)). (cl4tac r truegoal). Figure 5: A tactic-style encoding of some propositional definite clauses tional goal formulas that will be considered to be conjunctions of propositions. The objective will, of course, be to prove such formulas. Each primitive object-level goal therefore corresponds to showing some atomic proposition to be true, and such a goal might be encoded by a... Educational Role Student ♦ Teacher Age Range above 22 year Educational Use Research Education Level UG and PG ♦ Career/Technical Study Learning Resource Type Article Publisher Date 1986-01-01 Publisher Institution 3rd Int. Conf. Logic Programming, LNCS 225