Exemplos de formalizações

[arademaker]

Pessoal,

Em duplas, tentem bolar exemplos como do cap 3!

[danfol04]

Como discutido na última aula, iniciarei um exemplo. No clima do RJ, farei representação do "mundo" da praia. Ainda não tenho dupla, então alguém sinta-se livre para ajudar, corrigir e complementar.

Predicatos unários:

Homem()
Mulher()

Adulto()

Local()
Turista()

Banhista()
Trabalhador()
Ladrão()
Esportista()

VendedorBarraca()
VendedorQuiosque()
VendedorAmbulante()

Comida()
Bebida()
Objeto()

Nadar()
TomarSol()
Correr()
JogarFutevolei()

Pessoa()
Coisa()
Atos()

Predicatos n-ários:

Vendeu(i,n,m)
Roubou(i,n)

Exemplos: Vendeu(Pedro, João, Matte), Roubou(Pedro, João)

Correlações:

∀x[Adulto(x)⊃Pessoa(x)]
∀x[(Banhista(x)∨Trabalhador(x)∨Ladrão(x)∨Esportista(x))⊃Pessoa(x)]
∀x[(Local(x)∨Turista(x))⊃Pessoa(x)]
∀x[(Nadar(x)∨TomarSol(x)∨Correr(x)∨JogarFutevolei(x))⊃Ato(x)]
∀x[(Objeto(x)∨Bebida(x)∨Comida(x))⊃Coisa(x)]

∀x[(Pessoa(x))∧Homem(x) ⊃ ¬Mulher(x)]
∀x[(Pessoa(x))∧Turista(x) ⊃ ¬Local(x)]
∀x[(Pessoa(x))∧VendedorAmbulante(x) ⊃ ¬VendedorQuiosque(x)]
∀x[(Pessoa(x))∧Adulto(x) ⊃ (Homem(x) ∨ Mulher(x))]
∀y[(Pessoa(y))∧(VendedorBarraca( y) ∨ VendedorQuiosque( y) ∨ VendedorAmbulante( y)) ⊃ Trabalhador( y)]
∀y[(Pessoa(y))∧Trabalhador( y) ⊃ (VendedorBarraca( y) ∨ VendedorQuiosque( y) ∨ VendedorAmbulante( y))]
∀y[(Pessoa(y))∧(¬VendedorBarraca( y) ∨ ¬VendedorQuiosque( y) ∨ ¬VendedorAmbulante( y)) ⊃ (Banhista(y) ∨ Ladrão(y) ∨ Esportista(y))]
∀y∃x,z[(Pessoa(y)∧Pessoa(x)∧Coisa(z)))∧Vendeu(y,x,z)⊃Trabalhador(y)]
∀y∃x[(Pessoa(y)∧Pessoa(x))∧Roubou(y,x)⊃Ladrão(y)]
∀y[(Pessoa(y))∧Esportista(y)⊃(Nadar(y) ∨ Correr(y) ∨ JogarFutevolei(y))]

Questões:

Prove que existe um vendedor ambulante que vendeu matte para Pedro.

∀y∃x,z[(Pessoa(y)∧Pessoa(x)∧Coisa(z)))∧Vendeu(y,x,z)⊃Trabalhador(y)]
∀y[(Pessoa(y))∧Trabalhador( y) ⊃ (VendedorBarraca( y) ∨ VendedorQuiosque( y) ∨ VendedorAmbulante( y))]

Prove que existe um vendedor de quiosque que foi roubado por um ladrão.

∀y[(Pessoa(y))∧(VendedorBarraca( y) ∨ VendedorQuiosque( y) ∨ VendedorAmbulante( y)) ⊃ Trabalhador( y)]
∀x[(Banhista(x)∨Trabalhador(x)∨Ladrão(x)∨Esportista(x))⊃Pessoa(x)]
∀y∃x[(Pessoa(y)∧Pessoa(x))∧Roubou(y,x)⊃Ladrão(y)]

[odanoburu]

check #3 for my contribution.

[odanoburu]

I made a new PR (#4), correcting my previous mistakes and clearing up the proofs (except for item c, which I'm not sure I got right).

I've added a tptp version of the problem too. eprover says it's found a proof to it, but I'm not sure where in the output it is.

[odanoburu]

btw, after I half-broke my machine yesterday trying to compile eprover I found out we can query the tptp website to solve problems:

• here you find a syntax checker

• and here we have several solvers available, including eprover and SNARK

[hfcmf]

Aluno: Hélio Macedo FORMALIZAÇÃO – LÓGICA – PARTIDA DE FUTEBOL

PREDICADOS UNÁRIOS

• Jogadores
• Torcedores
• Técnico
• Campeonato

PREDICADOS N-ÁRIOS

• Jogar
• Contente
• Culpa

ARGUMENTOS (1) Se o time joga bem, ganha o campeonato. (2) Se o time não joga bem, o técnico é culpado. (3) Se o time ganha o campeonato, os torcedores ficam contentes. (4) Os torcedores não estão contentes. (5) Logo, o técnico é culpado.

ASSOCIAÇÃO DE PROPOSIÇÃO p : “o time joga bem” q : “o time ganha o campeonato” r : “o técnico ´e culpado” s : “os torcedores ficam contentes”

(1) p → q (2) ¬p → r (3) q → s {p → q, ¬p → r, q → s, ¬s} |= r, (4) ¬s (5) r

[arademaker]

@hfcmf excelente. Tente fazer um PR e codificar o problema em TPTP ou SNARK ? Tente formular 'perguntas' para sua teoria, isto é, quais implicações temos a partir da sua formalização?

[danfol04]

http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=PUZ&File=PUZ027-1.p

Problem:

There is an island with exactly three types of people -truthtellers who always tell the truth, and liars who always lie, and normals who sometimes tell the truth and sometimes lie. Liars are said to be of the lowest rank, normals are middle rank, and truthtellers of the highest rank. Two people A and B on the island make the following statements. A: I am of lower rank than B. B: That's not true! What are the ranks of A and B, and which of the two statements are true?

Proposições:

A1: "A is a truthteller" → "A is of the highest rank" A2: "A is middle rank" A3: "A is a liar" → "A is of the lowest rank" AT: "A is saying the truth" AL "A is lying" A1 → AT A3 → AL A2 → (AT∨AL)

B1: "B is a truthteller" -> "B is of the highest rank" B2: "B is middle rank" B3: "B is a liar" -> "B is of the lowest rank" BT: "B is saying the truth" BL "B is lying" B1 → BT B3 → BL B2 → (BT∨BL)

(i) If A1, then A told the truth and B must be of a higher rank. However, A is already in the highest one. Then, A1 is FALSE! (A1 → AT; (AT∧A1) → ¬(B1∨B2∨B3))

(ii) if A3, then A lied and B must be of the same rank or a lower one. (ii.1) B has a lower rank: This is FALSE, because A is already of the lowest rank. (A3 → AL; (AL∧A3) → ¬(B1∨B2∨B3)) (ii.2) B has the same rank (A3 -> B3): This is also FALSE, because B3 implies that B was lying (B3 → BL). In other words, A was supposed to be telling the truth, which is the opposite of the premise required to A3 be true. (A3 → AL; B3 → BL; BL → AT; AT → ¬A3) Then, A3 is FALSE!

(iii) A2 must be TRUE! Then, A can be saying the truth or lying (A2 → (AT∨AL)). (iii.1) (A2∧AT) → B1; B1 → BT; BT → ¬AT. Then, AT is FALSE! (iii.2) (A2∧AL) → (B2∨B3); B3 → BL; BL → ¬AL → ¬(A2∧AL). Then, B3 is FALSE! B2 → (BT∨BL); BT → AL, which is TRUE. If B3 and B1 are FALSE, B2 must be TRUE. Then, A2 and B2 are TRUE!

Answer:

A2 and B2 are TRUE. A and B are of middle rank. In this case, A is lying and B is saying the truth!

---

Understanding the Code:

cnf(not_lower_is_irreflexive,axiom, ( a_truth(not_lower(X,X)) )).

For any X and Y, X cannot be lower than itself.

cnf(not_not_lower_and_lower,axiom, ( ~ a_truth(not_lower(X,Y)) | ~ a_truth(lower(X,Y)) )).

For any X and Y, X can't be lower and not lower than Y at the same time.

cnf(not_lower_or_lower,axiom, ( a_truth(not_lower(X,Y)) | a_truth(lower(X,Y)) )).

For any X and Y, X must be lower or not lower than Y.

cnf(liars_lowest,axiom, ( ~ a_truth(lower(X,Y)) | ~ a_truth(liar(X)) | a_truth(normal(Y)) | a_truth(truthteller(Y)) )).

For any X and Y, if X is lower than Y and X is a liar, then Y must be normal or a truthteller.

cnf(truthtellers_highest,axiom, ( ~ a_truth(lower(X,Y)) | ~ a_truth(normal(X)) | a_truth(truthteller(Y)) )).

For any X and Y, If X is lower than Y and X is normal, then Y must be a truthteller.

cnf(truthtellers_lower_than_no_one,axiom, ( ~ a_truth(lower(X,Y)) | ~ a_truth(truthteller(X)) )).

For any X and Y, X cannot be lower than Y and a truthteller at the same time (exactly because truthtellers are lower than no one).

cnf(normal_and_liars_lower_than_truthtellers,axiom, ( ~ a_truth(lower(X,Y)) | ~ a_truth(truthteller(Y)) | a_truth(normal(X)) | a_truth(liar(X)) )).

For any X and Y, if X is lower than Y and Y is a truthteller, then X must be normal or a liar.

cnf(liars_lower_than_normal,axiom, ( ~ a_truth(lower(X,Y)) | ~ a_truth(normal(Y)) | a_truth(liar(X)) )).

For any X and Y, if X is lower than Y and Y in normal, then X must be a liar.

cnf(no_one_lower_than_liars,axiom, ( ~ a_truth(lower(X,Y)) | ~ a_truth(liar(Y)) )).

For any X and Y, X cannot be lower than Y if Y is a liar (exactly because liars are not lower than anyone else).

cnf(not_lower_than_truthteller,axiom, ( ~ a_truth(not_lower(X,Y)) | ~ a_truth(truthteller(X)) | a_truth(truthteller(Y)) | a_truth(lower(Y,X)) )).

For any X and Y, if X is not lower than Y and X is a truthteller, so Y is also a truthteller or Y is lower than X (which means that he can be normal or a liar).

cnf(not_lower_than_liar,axiom, ( ~ a_truth(not_lower(X,Y)) | ~ a_truth(liar(X)) | a_truth(liar(Y)) | a_truth(lower(Y,X)) )).

For any X and Y, If X is not lower than Y and X is a liar, then Y is also a liar or lower than X (however, once liars are already the lowest ones, than Y can only be a liar).

cnf(not_lower_than_normal,axiom, ( ~ a_truth(not_lower(X,Y)) | ~ a_truth(normal(X)) | a_truth(normal(Y)) | a_truth(lower(Y,X)) )).

For any X and Y, if X is not lower than Y and X is normal, then Y is also normal or lower than X (which means, a liar).

cnf(a_says_a_lower_than_b,hypothesis, ( a_truth(says(a,lower(a,b))) )).

A says that A is lower than B

cnf(b_says_a_not_lower_than_b,hypothesis, ( a_truth(says(b,not_lower(a,b))) )).

B says that A is not lower than B (in other words, B is saying that A did not say the truth).