Lausearvutuse ja lihtsamate predikaatarvutuse ülesannete lahendamine

Allikas: Lambda

Do all of the following excercises:

Geoff notes page 13/14

Exercises: determine if each F is a logical consequence of the Axioms. Do some directly and some using unsatisfiability ...

Solve 4 of these (your own choice), including the last.

  • Some should be shown directly: show that the implication is a tautology
  • Some should be shown via unsatisfiability: show that the negation of the implication is contradictory

You can use the truth table or clever conversions.

Example of conversions without truth table: 

((p => q)  & (~q | p) & (p | q )) => (p & q)
((p => q)  & (q => p) & (p | q )) => (p & q)
we see that p is equivalent to q.
Then (p | q ) is equivalent to p and (p & q) is equivalent to p.
Rewrite the formula as: p => p

NB! You may want to use http://logik.phl.univie.ac.at/~chris/gateway/formular-uk-zentral.html

Geoff notes page 19 first

Encode the following task in first order logic. No need to prove that the consequence holds:

Wolves, foxes, birds, caterpillars, and snails are animals, and there are some of each of them. Also there are some grains, and grains are plants. Every animal either likes to eat all plants or all animals much smaller than itself that like to eat some plants. Caterpillars and snails are much smaller than birds, which are much smaller than foxes, which in turn are much smaller than wolves. Wolves do not like to eat foxes or grains, while birds like to eat caterpillars but not snails. Caterpillars and snails like to eat some plants. Prove that there is an animal that likes to eat a grain eating animal.

Some parts for starters

Wolf is an animal: forall X (wolf(X) => animal(X)).

There are some wolves: exists X (wolf(X)). Skolemized version: wolf(cw) where cw is a new constant.

Caterpillars are much smaller than birds: forall X, Y ((caterpillar(X) & bird(Y)) => ms(X,Y)).

Geoff notes page 19 second

The basic notion of set theory is membership of a set. Using a member/2 predicate, define set equality, intersection, union, empty set, and difference (power set not obligatory). Empty set is a constant. Set equality, intersection and union are functions on sets, returning a set. For example, intersection is defined as: 

forall [X,A,B] :
  ( member(X,intersection(A,B))
       <=> 
  ( member(X,A)  & member(X,B) )  )

Next, try to do at least one of these: write conjectures for associativity of set intersection, and distribution of intersection over union.

Example and a question

As an example, the transitivity of subset: forall X, Y, Z (subset(X,Y) & subset(Y,Z) => subset(X,Z)).

A question: is that correct and sufficient to define a subset? forall X,Y,Z ((member(X,Y) => member(X,Z)) => subset(Y,Z)) ????

Loogikaõpik lk 127

Formaliseerige koolimatemaatika väited. (Allikad: III, IV ja V klassi õpikud, 1987–1990.). Piisab pooltest.

  • (a) Summa ei muutu, kui muudame liidetavate järjekorda.
  • (b) Kui summast lahutame ühe liidetava, siis saame teise liidetava.
  • (c) Korrutis ei muutu, kui muudame tegurite järjekorda.
  • (d) Kui üks tegur on võrdne 1-ga, siis korrutis on võrdne

teise teguriga.

  • (e) Kui üks tegur on võrdne nulliga, siis korrutis on võrdne

nulliga.

  • (f) Paarisarvule järgneb ja eelneb paaritu arv.
  • (g) Summa korrutamiseks arvuga võime korrutada liidetavad

eraldi ja korrutised liita.

  • (h) Selle asemel, et lahutada arvust summa, võin enne lahutada

ühe liidetava ja siis teise liidetava.

  • (i) Kui arvu ristsumma jagub 3-ga, siis arv jagub 3-ga, vastasel

juhul mitte.

Pane tähele

Eeldame, et meil on siin võrduspredikaat olemas.

Näitena esimene ülesanne: forall X,Y. sum(X,Y)=sum(Y,X).

Taustaks aritmeetika:

Arvud koostatakse nii: on olemas 0 ja funktsioon s (successor ehk ühe liitmine). Arvud 0,1,2, ... kodeeritakse kui 0, s(0), s(s(0)), ...

Liitmise defineerime induktiivselt niimoodi: 

forall X     +(0,X) = X.
forall X,Y  +(s(X),Y) = s(+(X,Y)) .

Geoff notes page 22 nr 11 second

Given the 1 st order logic language: V = { V : V starts with uppercase } F = { holden/0, ford/0, honda/0 main_competitor/1 } P = { fast/1, faster/2 } and the interpretation: ...

Show the steps of the interpretation of:

  • faster(main_competitor(laser),commodore)
  • fast(main_competitor(main_competitor(prelude))
  • forall X ( faster(main_competitor(X),laser) & fast(X) )
  • exists X ( fast(main_competitor(main_competitor(X))) | forall Y faster(X,Y) ) )

Example: first formula

faster(main_competitor(laser),commodore)
faster(prelude,commodore)
FALSE
Pärit leheküljelt "http://lambda.ee/w/index.php?title=Lausearvutuse_ja_lihtsamate_predikaatarvutuse_ülesannete_lahendamine&oldid=12224"