Fdtxjr

What is the difference between "behavior" and "behaviour"?

Roman Numeral Treatment of Suspensions

Why are there no referendums in the US?

How can I kill an app using Terminal?

Is there a problem with hiding "forgot password" until it's needed?

Unreliable Magic - Is it worth it?

How does Loki do this?

Was Spock the First Vulcan in Starfleet?

CREATE opcode: what does it really do?

What is the best translation for "slot" in the context of multiplayer video games?

Applicability of Single Responsibility Principle

Is `x >> pure y` equivalent to `liftM (const y) x`

Why not increase contact surface when reentering the atmosphere?

Hostile work environment after whistle-blowing on coworker and our boss. What do I do?

Would this custom Sorcerer variant that can only learn any verbal-component-only spell be unbalanced?

How do scammers retract money, while you can’t?

Do the temporary hit points from the Battlerager barbarian's Reckless Abandon stack if I make multiple attacks on my turn?

Trouble understanding the speech of overseas colleagues

Purchasing a ticket for someone else in another country?

How easy is it to start Magic from scratch?

How does the UK government determine the size of a mandate?

Did the DC-9 ever use RATO in revenue service?

Is there a korbon needed for conversion?

I'm in charge of equipment buying but no one's ever happy with what I choose. How to fix this?

Need help proving this entailment where the KB has sentences with multiple conjuncts

Need Help with Propositional LogicNeed help with propositional logic [Proof]Propositional resolution: the correct way to proceedResolution refutation of a tautology not resolving.Help with converting sentences into predicate logicStrong completeness of resolution in Boolean/propositional logicDiscrete Math: Resolution rule questionDetermine both the conjunctive and disjunctive normal forms for the following expression [verification]Need help simplifying this Boolean expressionNeed help formalising simple propositional logic sentences

0

$begingroup$

Show formally (using a proof rather than a Truth Table) that A follows from the given sentences shown.

1. P ∧ Z


2. (¬R ∧ ¬W) ∨ (¬P)


3. (W ∧ Q) ⇒ P


4. Q ∨ W


5. Q ⇒ (A ∨ P)


6. (P ∧ Q) ⇒ (A ∨ R)

In other words, we need to prove KB ⊨ A, where KB is the collection of sentences. I'll use Resolution Theorem Proving for this proof, and to prove that KB ⊨ A, we need to show that KB ∧ ¬A is unsatisfiable. That is, KB ∧ ¬A is True in NO models.

Resolution Theorem Proving Steps:

Convert KB ∧ ¬A into CNF

1. Apply the resolution rule whenever possible and add the result as an additional clause in the conjunction


2. Repeat step 2 until either:
   a. No new clauses can be added: KB does not entail A
   b. Two clauses resolve to yield the empty clause: KB entails A

Converting the KB to CNF:

Number Sentence

1 P ∧ Z given, already in CNF

1 (P) ∧ (Z) Associativity

2 (¬R ∧ ¬W) ∨ (¬P) Given

2 (¬R ∨ ¬P) ∧ (¬W ∨ ¬P) Distributivity of ∨ over ∧

3 (W ∧ Q) ⇒ P Given

3 ¬(W ∧ Q) ∨ P Implication elimination

3 (¬W ∨ ¬Q) ∨ P DeMorgan

3 (¬W ∨ ¬Q ∨ P) Associativity, now in CNF

4 Q ∨ W Given

4 (Q ∨ W) Associativity

5 Q ⇒ (A ∨ P) Given

5 ¬Q ∨ (A ∨ P) Implication elimination

5 (¬Q ∨ A ∨ P) Associativity

6 (P ∧ Q) ⇒ (A ∨ R) Given

6 ¬(P ∧ Q) ∨ (A ∨ R) Implication Elimination

6 (¬P ∨ ¬Q) ∨ (A ∨ R) DeMorgan

6 (¬P ∨ ¬Q ∨ A ∨ R) Associativity

7 ¬A Negated query

KB in CNF:

1 (P) ∧ (Z)

2 (¬R ∨ ¬P) ∧ (¬W ∨ ¬P)

3 (¬W ∨ ¬Q ∨ P)

4 (Q ∨ W)

5 (¬Q ∨ A ∨ P)

6 (¬P ∨ ¬Q ∨ A ∨ R)

7 ¬A

I'm stuck at how to come up with a contradiction. Mainly stuck in resolving variables where there are two conjuncts as in (¬R ∨ ¬P) ∧ (¬W ∨ ¬P) (2) and (P) ∧ (Z) (1).

propositional-calculus

share|cite|improve this question

edited Mar 18 at 15:30

Leonardo Lopez

asked Mar 17 at 22:39

Leonardo LopezLeonardo Lopez

1054

$endgroup$

add a comment | 

0

$begingroup$

Show formally (using a proof rather than a Truth Table) that A follows from the given sentences shown.

1. P ∧ Z


2. (¬R ∧ ¬W) ∨ (¬P)


3. (W ∧ Q) ⇒ P


4. Q ∨ W


5. Q ⇒ (A ∨ P)


6. (P ∧ Q) ⇒ (A ∨ R)

In other words, we need to prove KB ⊨ A, where KB is the collection of sentences. I'll use Resolution Theorem Proving for this proof, and to prove that KB ⊨ A, we need to show that KB ∧ ¬A is unsatisfiable. That is, KB ∧ ¬A is True in NO models.

Resolution Theorem Proving Steps:

Convert KB ∧ ¬A into CNF

1. Apply the resolution rule whenever possible and add the result as an additional clause in the conjunction


2. Repeat step 2 until either:
   a. No new clauses can be added: KB does not entail A
   b. Two clauses resolve to yield the empty clause: KB entails A

Converting the KB to CNF:

Number Sentence

1 P ∧ Z given, already in CNF

1 (P) ∧ (Z) Associativity

2 (¬R ∧ ¬W) ∨ (¬P) Given

2 (¬R ∨ ¬P) ∧ (¬W ∨ ¬P) Distributivity of ∨ over ∧

3 (W ∧ Q) ⇒ P Given

3 ¬(W ∧ Q) ∨ P Implication elimination

3 (¬W ∨ ¬Q) ∨ P DeMorgan

3 (¬W ∨ ¬Q ∨ P) Associativity, now in CNF

4 Q ∨ W Given

4 (Q ∨ W) Associativity

5 Q ⇒ (A ∨ P) Given

5 ¬Q ∨ (A ∨ P) Implication elimination

5 (¬Q ∨ A ∨ P) Associativity

6 (P ∧ Q) ⇒ (A ∨ R) Given

6 ¬(P ∧ Q) ∨ (A ∨ R) Implication Elimination

6 (¬P ∨ ¬Q) ∨ (A ∨ R) DeMorgan

6 (¬P ∨ ¬Q ∨ A ∨ R) Associativity

7 ¬A Negated query

KB in CNF:

1 (P) ∧ (Z)

2 (¬R ∨ ¬P) ∧ (¬W ∨ ¬P)

3 (¬W ∨ ¬Q ∨ P)

4 (Q ∨ W)

5 (¬Q ∨ A ∨ P)

6 (¬P ∨ ¬Q ∨ A ∨ R)

7 ¬A

I'm stuck at how to come up with a contradiction. Mainly stuck in resolving variables where there are two conjuncts as in (¬R ∨ ¬P) ∧ (¬W ∨ ¬P) (2) and (P) ∧ (Z) (1).

propositional-calculus

share|cite|improve this question

edited Mar 18 at 15:30

Leonardo Lopez

asked Mar 17 at 22:39

Leonardo LopezLeonardo Lopez

1054

$endgroup$

add a comment | 

$begingroup$

Show formally (using a proof rather than a Truth Table) that A follows from the given sentences shown.

1. P ∧ Z


2. (¬R ∧ ¬W) ∨ (¬P)


3. (W ∧ Q) ⇒ P


4. Q ∨ W


5. Q ⇒ (A ∨ P)


6. (P ∧ Q) ⇒ (A ∨ R)

In other words, we need to prove KB ⊨ A, where KB is the collection of sentences. I'll use Resolution Theorem Proving for this proof, and to prove that KB ⊨ A, we need to show that KB ∧ ¬A is unsatisfiable. That is, KB ∧ ¬A is True in NO models.

Resolution Theorem Proving Steps:

Convert KB ∧ ¬A into CNF

1. Apply the resolution rule whenever possible and add the result as an additional clause in the conjunction


2. Repeat step 2 until either:
   a. No new clauses can be added: KB does not entail A
   b. Two clauses resolve to yield the empty clause: KB entails A

Converting the KB to CNF:

Number Sentence

1 P ∧ Z given, already in CNF

1 (P) ∧ (Z) Associativity

2 (¬R ∧ ¬W) ∨ (¬P) Given

2 (¬R ∨ ¬P) ∧ (¬W ∨ ¬P) Distributivity of ∨ over ∧

3 (W ∧ Q) ⇒ P Given

3 ¬(W ∧ Q) ∨ P Implication elimination

3 (¬W ∨ ¬Q) ∨ P DeMorgan

3 (¬W ∨ ¬Q ∨ P) Associativity, now in CNF

4 Q ∨ W Given

4 (Q ∨ W) Associativity

5 Q ⇒ (A ∨ P) Given

5 ¬Q ∨ (A ∨ P) Implication elimination

5 (¬Q ∨ A ∨ P) Associativity

6 (P ∧ Q) ⇒ (A ∨ R) Given

6 ¬(P ∧ Q) ∨ (A ∨ R) Implication Elimination

6 (¬P ∨ ¬Q) ∨ (A ∨ R) DeMorgan

6 (¬P ∨ ¬Q ∨ A ∨ R) Associativity

7 ¬A Negated query

KB in CNF:

1 (P) ∧ (Z)

2 (¬R ∨ ¬P) ∧ (¬W ∨ ¬P)

3 (¬W ∨ ¬Q ∨ P)

4 (Q ∨ W)

5 (¬Q ∨ A ∨ P)

6 (¬P ∨ ¬Q ∨ A ∨ R)

7 ¬A

I'm stuck at how to come up with a contradiction. Mainly stuck in resolving variables where there are two conjuncts as in (¬R ∨ ¬P) ∧ (¬W ∨ ¬P) (2) and (P) ∧ (Z) (1).

propositional-calculus

share|cite|improve this question

edited Mar 18 at 15:30

Leonardo Lopez

asked Mar 17 at 22:39

Leonardo LopezLeonardo Lopez

1054

$endgroup$

share|cite|improve this question

edited Mar 18 at 15:30

Leonardo Lopez

asked Mar 17 at 22:39

Leonardo LopezLeonardo Lopez

1054

share|cite|improve this question

edited Mar 18 at 15:30

Leonardo Lopez

asked Mar 17 at 22:39

Leonardo LopezLeonardo Lopez

1054

asked Mar 17 at 22:39

Leonardo LopezLeonardo Lopez

1054

asked Mar 17 at 22:39

Leonardo LopezLeonardo Lopez

1054

1 Answer
1

active

oldest

votes

1

$begingroup$

As usual, we have to remove $land$ and $to$, using many times Material Implication equivalence as well as Distributivity on 2) to get:

1a) $P$

1b) $Z$

2a) $¬R ∨ ¬P$

2b) $¬W ∨ ¬P$

3) $¬ W ∨ ¬Q ∨ P$

4) $Q ∨ W$

5) $¬Q ∨ A ∨ P$

6) $¬P ∨ ¬Q ∨ A ∨ R$

7) $¬A$

---

Now apply Resolution to 1a) and 2a) to get $¬R$ and 1a) and 2b) to get $¬W$.

Use $¬W$ with 4) to get $Q$.

Finally, use $P, Q$ and $¬R$ with 6) to get $A$.

share|cite|improve this answer

answered Mar 18 at 7:38

Mauro ALLEGRANZAMauro ALLEGRANZA

67.5k449117

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Is it allowed to use the same sentence, say 1a, twice to form new sentences?
  $endgroup$
  – Leonardo Lopez
  Mar 18 at 15:33
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  @LeonardoLopez - the Resolution proof procedure is aimed at automated theorem proving (i.e. to be performed by a machine) : "The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals."
  $endgroup$
  – Mauro ALLEGRANZA
  Mar 18 at 15:38
  

  
  
  
  

add a comment | 

Your Answer

StackExchange.ifUsing("editor", function ()
return StackExchange.using("mathjaxEditing", function ()
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix)
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
);
);
, "mathjax-editing");

StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "69"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);

StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);

else
createEditor();

);

function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader:
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
,
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);



);

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name

Email

Required, but never shown

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3152173%2fneed-help-proving-this-entailment-where-the-kb-has-sentences-with-multiple-conju%23new-answer', 'question_page');

);

Post as a guest

Name

Email

Required, but never shown

1

$begingroup$

As usual, we have to remove $land$ and $to$, using many times Material Implication equivalence as well as Distributivity on 2) to get:

1a) $P$

1b) $Z$

2a) $¬R ∨ ¬P$

2b) $¬W ∨ ¬P$

3) $¬ W ∨ ¬Q ∨ P$

4) $Q ∨ W$

5) $¬Q ∨ A ∨ P$

6) $¬P ∨ ¬Q ∨ A ∨ R$

7) $¬A$

---

Now apply Resolution to 1a) and 2a) to get $¬R$ and 1a) and 2b) to get $¬W$.

Use $¬W$ with 4) to get $Q$.

Finally, use $P, Q$ and $¬R$ with 6) to get $A$.

share|cite|improve this answer

answered Mar 18 at 7:38

Mauro ALLEGRANZAMauro ALLEGRANZA

67.5k449117

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Is it allowed to use the same sentence, say 1a, twice to form new sentences?
  $endgroup$
  – Leonardo Lopez
  Mar 18 at 15:33
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  @LeonardoLopez - the Resolution proof procedure is aimed at automated theorem proving (i.e. to be performed by a machine) : "The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals."
  $endgroup$
  – Mauro ALLEGRANZA
  Mar 18 at 15:38
  

  
  
  
  

add a comment | 

1

$begingroup$

As usual, we have to remove $land$ and $to$, using many times Material Implication equivalence as well as Distributivity on 2) to get:

1a) $P$

1b) $Z$

2a) $¬R ∨ ¬P$

2b) $¬W ∨ ¬P$

3) $¬ W ∨ ¬Q ∨ P$

4) $Q ∨ W$

5) $¬Q ∨ A ∨ P$

6) $¬P ∨ ¬Q ∨ A ∨ R$

7) $¬A$

---

Now apply Resolution to 1a) and 2a) to get $¬R$ and 1a) and 2b) to get $¬W$.

Use $¬W$ with 4) to get $Q$.

Finally, use $P, Q$ and $¬R$ with 6) to get $A$.

share|cite|improve this answer

answered Mar 18 at 7:38

Mauro ALLEGRANZAMauro ALLEGRANZA

67.5k449117

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Is it allowed to use the same sentence, say 1a, twice to form new sentences?
  $endgroup$
  – Leonardo Lopez
  Mar 18 at 15:33
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  @LeonardoLopez - the Resolution proof procedure is aimed at automated theorem proving (i.e. to be performed by a machine) : "The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals."
  $endgroup$
  – Mauro ALLEGRANZA
  Mar 18 at 15:38
  

  
  
  
  

add a comment | 

$begingroup$

As usual, we have to remove $land$ and $to$, using many times Material Implication equivalence as well as Distributivity on 2) to get:

1a) $P$

1b) $Z$

2a) $¬R ∨ ¬P$

2b) $¬W ∨ ¬P$

3) $¬ W ∨ ¬Q ∨ P$

4) $Q ∨ W$

5) $¬Q ∨ A ∨ P$

6) $¬P ∨ ¬Q ∨ A ∨ R$

7) $¬A$

---

Now apply Resolution to 1a) and 2a) to get $¬R$ and 1a) and 2b) to get $¬W$.

Use $¬W$ with 4) to get $Q$.

Finally, use $P, Q$ and $¬R$ with 6) to get $A$.

share|cite|improve this answer

answered Mar 18 at 7:38

Mauro ALLEGRANZAMauro ALLEGRANZA

67.5k449117

$endgroup$

share|cite|improve this answer

answered Mar 18 at 7:38

Mauro ALLEGRANZAMauro ALLEGRANZA

67.5k449117

answered Mar 18 at 7:38

Mauro ALLEGRANZAMauro ALLEGRANZA

67.5k449117

answered Mar 18 at 7:38

Mauro ALLEGRANZAMauro ALLEGRANZA

67.5k449117