Programming Language Theory: Difference between revisions

@@ Line 131: / Line 131: @@
 ** Resolvent grows when a RHS is substituted for a subgoal
 ** Resolvent shrinks when a fact matches a subgoal
+** ''Logically-incomplete'': DFS might fail on left-recursive rules. BFS takes up a great deal of space.
+* The declarative semantics reduce the resolvent processing to modus ponens:
+** Any Prolog program can be represented as a set of Horn clauses...which can be transformed into clausal predicate logic...which can be transformed into predicate logic
+** A Horn clause is a set of terms, exactly one of which is positive
+*** A clause with no negative terms corresponds to a Prolog fact
+*** The single positive term corresponds to the LHS of a Prolog rule
+*** The zero or more negative terms correspond to clauses on the RHS
+{|
+! Prolog statement
+! Logical interpretation
+! Horn clause
+|-
+| A :- B || B ⇒ A || ~B ∨ A
+|}
 ===Constraint Programming===