Scribd Logo
Upload

Welcome to Scribd!

  • 32 views

    Programming Paradigms CSI2120: Jochen Lang EECS, University of Ottawa Canada

    Uploaded by

    aziz spam
    The document discusses the logic programming paradigm of Prolog. It covers predicate calculus, which uses predicates and Horn clauses. Prolog uses proof by contradiction and resolution to determine if predicates are true or false. It also discusses search trees for solving goals, with backtracking allowing Prolog to try alternative paths when it reaches a failure node.

    Copyright:

    © All Rights Reserved
    Download as PDF, TXT or read online from Scribd

    Programming Paradigms CSI2120: Jochen Lang EECS, University of Ottawa Canada

    Uploaded by

    aziz spam
    32 views19 pages
    The document discusses the logic programming paradigm of Prolog. It covers predicate calculus, which uses predicates and Horn clauses. Prolog uses proof by contradiction and resolution to determine if predicates are true or false. It also discusses search trees for solving goals, with backtracking allowing Prolog to try alternative paths when it reaches a failure node.

    Original Title

    7. Prolog_proofs

    Copyright

    © © All Rights Reserved

    Available Formats

    PDF, TXT or read online from Scribd

    Did you find this document useful?

    Is this content inappropriate?

    The document discusses the logic programming paradigm of Prolog. It covers predicate calculus, which uses predicates and Horn clauses. Prolog uses proof by contradiction and resolution to determine if predicates are true or false. It also discusses search trees for solving goals, with backtracking allowing Prolog to try alternative paths when it reaches a failure node.

    Copyright:

    © All Rights Reserved
    Download as PDF, TXT or read online from Scribd
    Download as pdf or txt
    32 views19 pages

    Programming Paradigms CSI2120: Jochen Lang EECS, University of Ottawa Canada

    Uploaded by

    aziz spam
    The document discusses the logic programming paradigm of Prolog. It covers predicate calculus, which uses predicates and Horn clauses. Prolog uses proof by contradiction and resolution to determine if predicates are true or false. It also discusses search trees for solving goals, with backtracking allowing Prolog to try alternative paths when it reaches a failure node.

    Copyright:

    © All Rights Reserved
    Download as PDF, TXT or read online from Scribd
    Download as pdf or txt
    You are on page 1of 19

    Programming

    Paradigms
    CSI2120

    Jochen Lang
    EECS, University of Ottawa
    Canada
    Logic Programming in Prolog

    • Predicate calculus
    – Predicates
    – Horn clauses
    – Proof by Contradiction: Resolution
    • Search Trees
    – Backtracking

    CSI2120: Programming Paradigms


    Prolog Predicates

    • A rule is a clause where the body is non-empty while a fact


    is a clause with an empty body. Most rules contain
    variables.
    • Prolog Definition with an anonymous variable, written as
    “_”
    salary(X) :- employed(Y,X). % Ok but with
    % a warning
    – Or with an anonymous variable
    salary(X) :- employed(_,X).
    • Facts and rules are predicates.

    CSI2120: Programming Paradigms


    Predicate Calculus

    • First Order Logic


    – predicate symbols: x,y,z (constants and variables)
    • and compound terms
    – equality: ≡
    – negation:
    – logic binary connections: ∨,∧, →
    – quantifiers ‘for all …’ and ‘there exists … such that’
    • universal quantifier ∀
    • existential quantifier ∃

    CSI2120: Programming Paradigms


    Predicates in Prolog

    • ← ∧ ∧ ⋯∧
    – All terms , , … , in the body of the predicate have to be
    true for the head to be true. Or, , , … , being true,
    implies b is true.
    • ←
    – This is a fact because truth is always implied.
    • ←
    – Without a head, it is goal for which correctness still needs to
    be proven. This may be considered a question in logic
    programming in Prolog. Proofing correctness requires
    deductive reasoning.

    CSI2120: Programming Paradigms


    Horn Clauses

    • We can express first order logic with Horn* clauses and


    solve predicate calculus mechanically
    • Horn clauses are the foundation of logic programming
    • Horn formulas are the only logic formulas in Prolog
    – Atomic (i.e., unique) formulas and their negation. They are
    also called literals.
    – Disjunction of literals to form clauses
    – A Horn clause has exactly one non-negated literal
    – Conjunctive normal form (CNF) is a conjunction of Horn
    clauses

    * Alfred Horn, 1918-2001 American Mathematician

    CSI2120: Programming Paradigms


    Converting to a Horn Formula

    • Implication (a implies b) ⟶ is the same as ∨


    • Equivalence (a equivalent to b) ≡ is the same as
    ∧ ∨ ∧
    • Example (Prolog): Proof f to be true.
    f :- a,b.
    a.
    b.
    • Predicate logic
    ( ∧ ⟶ ) and and
    • Horn formula
    ( ( ∧ ∨ )≡( ∨ ∨ )

    CSI2120: Programming Paradigms


    Proof by Resolution

    • Consider
    ( ∨ ∨ ) and and
    • Proof by contradiction, i.e., assume
    ( ∨ ∨ ) and and and
    • Simplify by resolution
    (( ∧ ∨ ∨ )) and and
    ∨ ) and and
    (( ∧ ∨ ) and
    and which is a contradiction

    CSI2120: Programming Paradigms


    Prolog and Horn Clauses

    • Facts and rules are Horn Clauses as in the example.


    • In general F :- F1, F2,…, Fn.
    – meaning F if F1 and F2 and …and Fn
    – F is an atomic formula
    – Fi are terms or their negation
    • F is the head of the clause
    • F1, F2,…, Fn together are the body of the clause
    • To prove F in Prolog, it must be true (proven) that F1, F2,…,
    and Fn are true .

    CSI2120: Programming Paradigms


    Horn Clauses

    • Horn clauses can express nearly all logic expressions, all


    mathematical algorithms.
    • It enables one to establish the truth of a hypothesis by
    establishing the truth of terms but it does not allow one to
    prove the falsehood of a hypothesis. False in logic
    programming only means that the goal can not be proven
    correct.

    CSI2120: Programming Paradigms


    Search Trees

    • Search trees represent queries


    – Root of the tree is the question
    – Nodes (or vertices) are decisions and show which goals still
    need to be satisfied
    – Transitions (along edges) from one node to the next are the
    result of an unification between a goal and a fact or the head
    of a rule.
    – The edges are a step in the proof.

    CSI2120: Programming Paradigms


    Nodes in Search Tree

    – Goals are ordered from left to right following the order in the
    rules. Goals are stated in a node.
    – Leaf nodes which contain one or several goals are failure
    nodes. The first (left-most) goal caused the failure.
    – Empty leaf nodes are success nodes. The path from the root
    to the leaf node contains the unifications and steps
    necessary for the proof. These can be found on the edges.

    CSI2120: Programming Paradigms


    Solution Strategy of Prolog

    • Prolog builds the search tree from the question as a root


    node. The tree is built in a depth-first fashion.
    • An empty (leaf) node is a proof or a solution
    – Search can continue for other solutions by backtracking and
    traversing unexplored branches
    • An non-empty leaf node is a failure
    – A solution may still be found by backtracking and traversing
    unexplored branches

    CSI2120: Programming Paradigms


    Backtracking

    • If there are no more new nodes found, there are no more


    solutions and Prolog answers no.
    • Termination is not guaranteed. It is easy to write rules that
    cause an infinite recursion.
    • The order in which solutions are produced depends on the
    order in predicates, in particular:
    – the order of the literals in the body of clause
    – the order of the predicates

    CSI2120: Programming Paradigms


    voter(Y)
    A Simple Example
    Y=X
    name(joe). name(X), citizen(X),
    name(jane). adult(X)
    citizen(jane). X=joe
    citizen(joe). X=jane
    citizen(joe), adult(joe)
    adult(jane).
    voter(X):- citizen(jane), adult(jane)
    name(X),
    citizen(X),
    adult(joe) adult(jane)
    adult(X).

    ?- voter(Y).

    CSI2120: Programming Paradigms


    Another Example

    Building categories:
    parent(building,farmbuilding).
    parent(farmbuilding,barn).
    parent(farmbuilding,silo).
    parent(farmbuilding,house).
    parent(barn,horsebarn).
    parent(barn,cowbarn).
    typeof(X,Y):- parent(Z,X),typeof(Z,Y).
    typeof(X,Y):- parent(Y,X).

    ?- typeof(cowbarn,A).

    CSI2120: Programming Paradigms


    Another Example: 3 Versions of French
    Nobleman
    Version C
    Version A father(charles,jean).
    father(charles,jean). noble(X):- father(Y,X),
    noble(henri). noble(Y).
    noble(louis). noble(henri).
    noble(charles). noble(louis).
    noble(X):- father(Y,X), noble(charles).
    noble(Y).
    Version B
    father(charles,jean).
    noble(henri).
    noble(louis).
    noble(charles).
    ?- noble(jean). noble(X):- noble(Y),
    father(Y,X).
    Source: R. Laganière

    CSI2120: Programming Paradigms


    A Last Example

    likes(peter,jane).
    likes(paul,jane).
    conflict(X,Y) :- likes(X,Z),likes(Y,Z).

    ?- conflict(X,Y).

    • How many solutions?

    CSI2120: Programming Paradigms


    Summary

    • Predicate calculus
    – Predicates
    – Horn clauses
    – Proof by Contradiction: Resolution
    • Search Trees
    – Backtracking

    CSI2120: Programming Paradigms

    You might also like