note ;;Quote: program via predicate logic defines a procedure as calls to other procedures plus terminal definitions

4 ;;Quote: a logic clause is the same as 'for all x1..xk B1 or ... or x1..xk Bm is implied by A1 and ... and An'

4+;;Quote: an atomic formula in a logic clause is a predicate over variables and functions of variables or functions of functions...

4 ;;Quote: implication in first-order logic can be replaced by unsatisfiability of sentences in clausal form

QuoteRef: kowaR11_1973 ;;5 Clausal definition of factorial: (F1) fact (0,1)<- (F2) Fact (x+1,u) <- Fact (x,v), Times (x+1, v, u) (F3) <- Fact (2,y) here y=2 (the solution) contradicts F1 and F2 since Fact (0,v) and Times (2, v, u) is true if v=1 (from Fact (0,1) and u=2 since Times (2,1,2)

6 ;;Quote: Horn clauses have a single antecedent; define procedures, assert facts, and specify goals

7 ;;Quote: can create a useful inference system from only resolution; like, matching procedure definitions to procedure calls

8 ;;Quote: a computation in logic programming consists of a sequence of goal statements derived from a set of Horn clauses

10 ;;Quote: logic programming is non-deterministic since a procedure call matches more than one definition

11 ;;Quote: in predicate logic, a procedure body is executed in any sequence

QuoteRef: kowaR11_1973 ;;12 if <-Fact (x,1) the contrainstance is x=0 or x=-1 this is non-deterministic and shows how input and output are done by how used

15 ;;Quote: viability of logic programming depends on an auxiliary control language for sequencing the proof procedure