Thumbnail
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