How to prove $(arightarrow negb)rightarrow(neg(b rightarrow c)rightarrow nega)$

Clash Royale CLAN TAG#URR8PPP

up vote
1
down vote

favorite

I'm trying to prove this by using Hilbert systems:

(CA1) ⊢ A → (B → A)

(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(MP) A, A → B ⊢ B

Is there a specific approach to these things that i'm not seeing ?

here is my approach but it's always hard for me to carry on from it :

From the given i see $Phi=arightarrownegbvdash neg(brightarrow c)rightarrow nega.$ By using the deduction theorem we recieve $Phicup neg(brightarrow c) =arightarrownegb,neg(brightarrow c)vdashneg a$ which needs to be proved to show that the original logic proposition is true.

Here i get stuck ,i try to solve this by saying that $nega$ then i try to see the previous steps that i need to to make to reach $nega$ for example if i do modus ponens on $varphi_1=neg(brightarrow c)$ and $varphi_2=neg(brightarrow c)rightarrow nega$ i will reach the end of the proof, but i think this is a bad approach for this.
I need help with ways to approach these kind of proofs.

logic propositional-calculus

share|cite|improve this question

asked Jul 23 at 11:50

user3133165

1618

• 
  
  
  

  
  

  
  
  
  
  
  

  
  What do you mean by "Prove $ p to q$"? Presumably you trying to show that $p to q$ is a tautology?
  – JavaMan
  Jul 23 at 13:29
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  I think so, sorry but the problem only states that to prove the given proposition by using those 3 axioms
  – user3133165
  Jul 23 at 13:42
  

  
  
  
  

add a comment | 

up vote
1
down vote

favorite

I'm trying to prove this by using Hilbert systems:

(CA1) ⊢ A → (B → A)

(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(MP) A, A → B ⊢ B

Is there a specific approach to these things that i'm not seeing ?

here is my approach but it's always hard for me to carry on from it :

From the given i see $Phi=arightarrownegbvdash neg(brightarrow c)rightarrow nega.$ By using the deduction theorem we recieve $Phicup neg(brightarrow c) =arightarrownegb,neg(brightarrow c)vdashneg a$ which needs to be proved to show that the original logic proposition is true.

Here i get stuck ,i try to solve this by saying that $nega$ then i try to see the previous steps that i need to to make to reach $nega$ for example if i do modus ponens on $varphi_1=neg(brightarrow c)$ and $varphi_2=neg(brightarrow c)rightarrow nega$ i will reach the end of the proof, but i think this is a bad approach for this.
I need help with ways to approach these kind of proofs.

logic propositional-calculus

share|cite|improve this question

asked Jul 23 at 11:50

user3133165

1618

• 
  
  
  

  
  

  
  
  
  
  
  

  
  What do you mean by "Prove $ p to q$"? Presumably you trying to show that $p to q$ is a tautology?
  – JavaMan
  Jul 23 at 13:29
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  I think so, sorry but the problem only states that to prove the given proposition by using those 3 axioms
  – user3133165
  Jul 23 at 13:42
  

  
  
  
  

add a comment | 

up vote
1
down vote

favorite

up vote
1
down vote

favorite

I'm trying to prove this by using Hilbert systems:

(CA1) ⊢ A → (B → A)

(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(MP) A, A → B ⊢ B

Is there a specific approach to these things that i'm not seeing ?

here is my approach but it's always hard for me to carry on from it :

From the given i see $Phi=arightarrownegbvdash neg(brightarrow c)rightarrow nega.$ By using the deduction theorem we recieve $Phicup neg(brightarrow c) =arightarrownegb,neg(brightarrow c)vdashneg a$ which needs to be proved to show that the original logic proposition is true.

Here i get stuck ,i try to solve this by saying that $nega$ then i try to see the previous steps that i need to to make to reach $nega$ for example if i do modus ponens on $varphi_1=neg(brightarrow c)$ and $varphi_2=neg(brightarrow c)rightarrow nega$ i will reach the end of the proof, but i think this is a bad approach for this.
I need help with ways to approach these kind of proofs.

logic propositional-calculus

share|cite|improve this question

asked Jul 23 at 11:50

user3133165

1618

I'm trying to prove this by using Hilbert systems:

(CA1) ⊢ A → (B → A)

(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(MP) A, A → B ⊢ B

Is there a specific approach to these things that i'm not seeing ?

here is my approach but it's always hard for me to carry on from it :

From the given i see $Phi=arightarrownegbvdash neg(brightarrow c)rightarrow nega.$ By using the deduction theorem we recieve $Phicup neg(brightarrow c) =arightarrownegb,neg(brightarrow c)vdashneg a$ which needs to be proved to show that the original logic proposition is true.

Here i get stuck ,i try to solve this by saying that $nega$ then i try to see the previous steps that i need to to make to reach $nega$ for example if i do modus ponens on $varphi_1=neg(brightarrow c)$ and $varphi_2=neg(brightarrow c)rightarrow nega$ i will reach the end of the proof, but i think this is a bad approach for this.
I need help with ways to approach these kind of proofs.

logic propositional-calculus

share|cite|improve this question

asked Jul 23 at 11:50

user3133165

1618

share|cite|improve this question

share|cite|improve this question

asked Jul 23 at 11:50

user3133165

1618

asked Jul 23 at 11:50

user3133165

1618

asked Jul 23 at 11:50

user3133165

1618

1618

• 
  
  
  

  
  

  
  
  
  
  
  

  
  What do you mean by "Prove $ p to q$"? Presumably you trying to show that $p to q$ is a tautology?
  – JavaMan
  Jul 23 at 13:29
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  I think so, sorry but the problem only states that to prove the given proposition by using those 3 axioms
  – user3133165
  Jul 23 at 13:42
  

  
  
  
  

add a comment | 

• 
  
  
  

  
  

  
  
  
  
  
  

  
  What do you mean by "Prove $ p to q$"? Presumably you trying to show that $p to q$ is a tautology?
  – JavaMan
  Jul 23 at 13:29
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  I think so, sorry but the problem only states that to prove the given proposition by using those 3 axioms
  – user3133165
  Jul 23 at 13:42
  

  
  
  
  

What do you mean by "Prove $ p to q$"? Presumably you trying to show that $p to q$ is a tautology?
– JavaMan
Jul 23 at 13:29

What do you mean by "Prove $ p to q$"? Presumably you trying to show that $p to q$ is a tautology?
– JavaMan
Jul 23 at 13:29

I think so, sorry but the problem only states that to prove the given proposition by using those 3 axioms
– user3133165
Jul 23 at 13:42

I think so, sorry but the problem only states that to prove the given proposition by using those 3 axioms
– user3133165
Jul 23 at 13:42

add a comment | 

1 Answer
1

active

oldest

votes

up vote
1
down vote

Here's a proof of a first-order proof using hyperresolution which correlates to a proof using condensed detachment from the theorem prover written by William McCune at Argonne National Laboratory. Also, instead of using infix notation, it uses prefix notation and letters. (x$rightarrow$y) translates to C(x, y) and $lnot$x translates to N(x):

% -------- Comments from original proof --------
% Proof 1 at 31.95 (+ 11.73) seconds.
% Length of proof is 44.
% Level of proof is 16.
% Maximum clause weight is 24.
% Given clauses 3400.

1 P(C(C(x,N(y)),C(N(C(y,z)),N(x)))) # label(non_clause) # label(goal). [goal].
2 -P(C(x,y)) | -P(x) | P(y). [assumption].
3 P(C(x,C(y,x))). [assumption].
4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))). [assumption].
5 P(C(C(N(x),N(y)),C(y,x))). [assumption].
6 -P(C(C(c1,N(c2)),C(N(C(c2,c3)),N(c1)))). [deny(1)].
7 P(C(x,C(y,C(z,y)))). [hyper(2,a,3,a,b,3,a)].
8 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))). [hyper(2,a,4,a,b,4,a)].
9 P(C(x,C(C(y,C(z,u)),C(C(y,z),C(y,u))))). [hyper(2,a,3,a,b,4,a)].
10 P(C(C(x,y),C(x,x))). [hyper(2,a,4,a,b,3,a)].
11 P(C(C(C(N(x),N(y)),y),C(C(N(x),N(y)),x))). [hyper(2,a,4,a,b,5,a)].
12 P(C(x,C(C(N(y),N(z)),C(z,y)))). [hyper(2,a,3,a,b,5,a)].
14 P(C(x,C(y,C(z,C(u,z))))). [hyper(2,a,3,a,b,7,a)].
17 P(C(x,x)). [hyper(2,a,10,a,b,7,a)].
18 P(C(C(C(x,y),x),C(C(x,y),y))). [hyper(2,a,4,a,b,17,a)].
26 P(C(C(x,C(C(y,x),z)),C(x,z))). [hyper(2,a,8,a,b,7,a)].
44 P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))). [hyper(2,a,8,a,b,14,a)].
48 P(C(C(C(x,C(y,z)),C(C(C(x,y),C(x,z)),u)),C(C(x,C(y,z)),u))). [hyper(2,a,8,a,b,9,a)].
71 P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))). [hyper(2,a,4,a,b,12,a)].
159 P(C(N(x),C(x,y))). [hyper(2,a,26,a,b,12,a)].
160 P(C(C(x,y),C(C(z,x),C(z,y)))). [hyper(2,a,26,a,b,9,a)].
166 P(C(x,C(N(y),C(y,z)))). [hyper(2,a,3,a,b,159,a)].
197 P(C(C(C(N(x),C(x,y)),z),z)). [hyper(2,a,18,a,b,166,a)].
815 P(C(C(C(x,y),z),C(y,z))). [hyper(2,a,44,a,b,160,a)].
835 P(C(x,C(C(C(y,z),u),C(z,u)))). [hyper(2,a,3,a,b,815,a)].
841 P(C(x,C(C(x,y),y))). [hyper(2,a,815,a,b,18,a)].
842 P(C(x,C(C(N(y),N(x)),y))). [hyper(2,a,815,a,b,11,a)].
918 P(C(C(x,y),C(x,C(C(y,z),z)))). [hyper(2,a,160,a,b,841,a)].
1299 P(C(C(x,C(N(y),N(x))),C(x,y))). [hyper(2,a,4,a,b,842,a)].
3180 P(C(C(x,C(y,z)),C(y,C(x,z)))). [hyper(2,a,48,a,b,835,a)].
4594 P(C(N(N(x)),x)). [hyper(2,a,197,a,b,1299,a)].
4644 P(C(N(N(x)),C(C(x,y),y))). [hyper(2,a,918,a,b,4594,a)].
4672 P(C(x,N(N(x)))). [hyper(2,a,5,a,b,4594,a)].
4728 P(C(C(x,y),C(x,N(N(y))))). [hyper(2,a,160,a,b,4672,a)].
7574 P(C(N(x),N(N(C(x,y))))). [hyper(2,a,197,a,b,4728,a)].
7977 P(C(N(C(x,y)),x)). [hyper(2,a,5,a,b,7574,a)].
8000 P(C(N(C(x,y)),C(C(x,z),z))). [hyper(2,a,918,a,b,7977,a)].
19593 P(C(C(x,y),C(N(C(x,z)),y))). [hyper(2,a,3180,a,b,8000,a)].
19609 P(C(C(x,y),C(N(N(x)),y))). [hyper(2,a,3180,a,b,4644,a)].
20519 P(C(C(x,N(y)),C(y,N(x)))). [hyper(2,a,71,a,b,19609,a)].
20805 P(C(x,C(C(y,N(x)),N(y)))). [hyper(2,a,3180,a,b,20519,a)].
21589 P(C(N(C(x,y)),C(C(z,N(x)),N(z)))). [hyper(2,a,19593,a,b,20805,a)].
29513 P(C(C(x,N(y)),C(N(C(y,z)),N(x)))). [hyper(2,a,3180,a,b,21589,a)].
29514 $F. [resolve(29513,a,6,a)].

share|cite|improve this answer

answered Jul 23 at 21:29

Doug Spoonwood

7,65012042

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',
convertImagesToLinks: true,
noModals: false,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
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

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2860265%2fhow-to-prove-a-rightarrow-negb-rightarrow-negb-rightarrow-c-rightarr%23new-answer', 'question_page');

);

Post as a guest

Name Email

1 Answer
1

active

oldest

votes

1 Answer
1

active

oldest

votes

active

oldest

votes

active

oldest

votes

up vote
1
down vote

Here's a proof of a first-order proof using hyperresolution which correlates to a proof using condensed detachment from the theorem prover written by William McCune at Argonne National Laboratory. Also, instead of using infix notation, it uses prefix notation and letters. (x$rightarrow$y) translates to C(x, y) and $lnot$x translates to N(x):

% -------- Comments from original proof --------
% Proof 1 at 31.95 (+ 11.73) seconds.
% Length of proof is 44.
% Level of proof is 16.
% Maximum clause weight is 24.
% Given clauses 3400.

1 P(C(C(x,N(y)),C(N(C(y,z)),N(x)))) # label(non_clause) # label(goal). [goal].
2 -P(C(x,y)) | -P(x) | P(y). [assumption].
3 P(C(x,C(y,x))). [assumption].
4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))). [assumption].
5 P(C(C(N(x),N(y)),C(y,x))). [assumption].
6 -P(C(C(c1,N(c2)),C(N(C(c2,c3)),N(c1)))). [deny(1)].
7 P(C(x,C(y,C(z,y)))). [hyper(2,a,3,a,b,3,a)].
8 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))). [hyper(2,a,4,a,b,4,a)].
9 P(C(x,C(C(y,C(z,u)),C(C(y,z),C(y,u))))). [hyper(2,a,3,a,b,4,a)].
10 P(C(C(x,y),C(x,x))). [hyper(2,a,4,a,b,3,a)].
11 P(C(C(C(N(x),N(y)),y),C(C(N(x),N(y)),x))). [hyper(2,a,4,a,b,5,a)].
12 P(C(x,C(C(N(y),N(z)),C(z,y)))). [hyper(2,a,3,a,b,5,a)].
14 P(C(x,C(y,C(z,C(u,z))))). [hyper(2,a,3,a,b,7,a)].
17 P(C(x,x)). [hyper(2,a,10,a,b,7,a)].
18 P(C(C(C(x,y),x),C(C(x,y),y))). [hyper(2,a,4,a,b,17,a)].
26 P(C(C(x,C(C(y,x),z)),C(x,z))). [hyper(2,a,8,a,b,7,a)].
44 P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))). [hyper(2,a,8,a,b,14,a)].
48 P(C(C(C(x,C(y,z)),C(C(C(x,y),C(x,z)),u)),C(C(x,C(y,z)),u))). [hyper(2,a,8,a,b,9,a)].
71 P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))). [hyper(2,a,4,a,b,12,a)].
159 P(C(N(x),C(x,y))). [hyper(2,a,26,a,b,12,a)].
160 P(C(C(x,y),C(C(z,x),C(z,y)))). [hyper(2,a,26,a,b,9,a)].
166 P(C(x,C(N(y),C(y,z)))). [hyper(2,a,3,a,b,159,a)].
197 P(C(C(C(N(x),C(x,y)),z),z)). [hyper(2,a,18,a,b,166,a)].
815 P(C(C(C(x,y),z),C(y,z))). [hyper(2,a,44,a,b,160,a)].
835 P(C(x,C(C(C(y,z),u),C(z,u)))). [hyper(2,a,3,a,b,815,a)].
841 P(C(x,C(C(x,y),y))). [hyper(2,a,815,a,b,18,a)].
842 P(C(x,C(C(N(y),N(x)),y))). [hyper(2,a,815,a,b,11,a)].
918 P(C(C(x,y),C(x,C(C(y,z),z)))). [hyper(2,a,160,a,b,841,a)].
1299 P(C(C(x,C(N(y),N(x))),C(x,y))). [hyper(2,a,4,a,b,842,a)].
3180 P(C(C(x,C(y,z)),C(y,C(x,z)))). [hyper(2,a,48,a,b,835,a)].
4594 P(C(N(N(x)),x)). [hyper(2,a,197,a,b,1299,a)].
4644 P(C(N(N(x)),C(C(x,y),y))). [hyper(2,a,918,a,b,4594,a)].
4672 P(C(x,N(N(x)))). [hyper(2,a,5,a,b,4594,a)].
4728 P(C(C(x,y),C(x,N(N(y))))). [hyper(2,a,160,a,b,4672,a)].
7574 P(C(N(x),N(N(C(x,y))))). [hyper(2,a,197,a,b,4728,a)].
7977 P(C(N(C(x,y)),x)). [hyper(2,a,5,a,b,7574,a)].
8000 P(C(N(C(x,y)),C(C(x,z),z))). [hyper(2,a,918,a,b,7977,a)].
19593 P(C(C(x,y),C(N(C(x,z)),y))). [hyper(2,a,3180,a,b,8000,a)].
19609 P(C(C(x,y),C(N(N(x)),y))). [hyper(2,a,3180,a,b,4644,a)].
20519 P(C(C(x,N(y)),C(y,N(x)))). [hyper(2,a,71,a,b,19609,a)].
20805 P(C(x,C(C(y,N(x)),N(y)))). [hyper(2,a,3180,a,b,20519,a)].
21589 P(C(N(C(x,y)),C(C(z,N(x)),N(z)))). [hyper(2,a,19593,a,b,20805,a)].
29513 P(C(C(x,N(y)),C(N(C(y,z)),N(x)))). [hyper(2,a,3180,a,b,21589,a)].
29514 $F. [resolve(29513,a,6,a)].

share|cite|improve this answer

answered Jul 23 at 21:29

Doug Spoonwood

7,65012042

add a comment | 

up vote
1
down vote

Here's a proof of a first-order proof using hyperresolution which correlates to a proof using condensed detachment from the theorem prover written by William McCune at Argonne National Laboratory. Also, instead of using infix notation, it uses prefix notation and letters. (x$rightarrow$y) translates to C(x, y) and $lnot$x translates to N(x):

% -------- Comments from original proof --------
% Proof 1 at 31.95 (+ 11.73) seconds.
% Length of proof is 44.
% Level of proof is 16.
% Maximum clause weight is 24.
% Given clauses 3400.

1 P(C(C(x,N(y)),C(N(C(y,z)),N(x)))) # label(non_clause) # label(goal). [goal].
2 -P(C(x,y)) | -P(x) | P(y). [assumption].
3 P(C(x,C(y,x))). [assumption].
4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))). [assumption].
5 P(C(C(N(x),N(y)),C(y,x))). [assumption].
6 -P(C(C(c1,N(c2)),C(N(C(c2,c3)),N(c1)))). [deny(1)].
7 P(C(x,C(y,C(z,y)))). [hyper(2,a,3,a,b,3,a)].
8 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))). [hyper(2,a,4,a,b,4,a)].
9 P(C(x,C(C(y,C(z,u)),C(C(y,z),C(y,u))))). [hyper(2,a,3,a,b,4,a)].
10 P(C(C(x,y),C(x,x))). [hyper(2,a,4,a,b,3,a)].
11 P(C(C(C(N(x),N(y)),y),C(C(N(x),N(y)),x))). [hyper(2,a,4,a,b,5,a)].
12 P(C(x,C(C(N(y),N(z)),C(z,y)))). [hyper(2,a,3,a,b,5,a)].
14 P(C(x,C(y,C(z,C(u,z))))). [hyper(2,a,3,a,b,7,a)].
17 P(C(x,x)). [hyper(2,a,10,a,b,7,a)].
18 P(C(C(C(x,y),x),C(C(x,y),y))). [hyper(2,a,4,a,b,17,a)].
26 P(C(C(x,C(C(y,x),z)),C(x,z))). [hyper(2,a,8,a,b,7,a)].
44 P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))). [hyper(2,a,8,a,b,14,a)].
48 P(C(C(C(x,C(y,z)),C(C(C(x,y),C(x,z)),u)),C(C(x,C(y,z)),u))). [hyper(2,a,8,a,b,9,a)].
71 P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))). [hyper(2,a,4,a,b,12,a)].
159 P(C(N(x),C(x,y))). [hyper(2,a,26,a,b,12,a)].
160 P(C(C(x,y),C(C(z,x),C(z,y)))). [hyper(2,a,26,a,b,9,a)].
166 P(C(x,C(N(y),C(y,z)))). [hyper(2,a,3,a,b,159,a)].
197 P(C(C(C(N(x),C(x,y)),z),z)). [hyper(2,a,18,a,b,166,a)].
815 P(C(C(C(x,y),z),C(y,z))). [hyper(2,a,44,a,b,160,a)].
835 P(C(x,C(C(C(y,z),u),C(z,u)))). [hyper(2,a,3,a,b,815,a)].
841 P(C(x,C(C(x,y),y))). [hyper(2,a,815,a,b,18,a)].
842 P(C(x,C(C(N(y),N(x)),y))). [hyper(2,a,815,a,b,11,a)].
918 P(C(C(x,y),C(x,C(C(y,z),z)))). [hyper(2,a,160,a,b,841,a)].
1299 P(C(C(x,C(N(y),N(x))),C(x,y))). [hyper(2,a,4,a,b,842,a)].
3180 P(C(C(x,C(y,z)),C(y,C(x,z)))). [hyper(2,a,48,a,b,835,a)].
4594 P(C(N(N(x)),x)). [hyper(2,a,197,a,b,1299,a)].
4644 P(C(N(N(x)),C(C(x,y),y))). [hyper(2,a,918,a,b,4594,a)].
4672 P(C(x,N(N(x)))). [hyper(2,a,5,a,b,4594,a)].
4728 P(C(C(x,y),C(x,N(N(y))))). [hyper(2,a,160,a,b,4672,a)].
7574 P(C(N(x),N(N(C(x,y))))). [hyper(2,a,197,a,b,4728,a)].
7977 P(C(N(C(x,y)),x)). [hyper(2,a,5,a,b,7574,a)].
8000 P(C(N(C(x,y)),C(C(x,z),z))). [hyper(2,a,918,a,b,7977,a)].
19593 P(C(C(x,y),C(N(C(x,z)),y))). [hyper(2,a,3180,a,b,8000,a)].
19609 P(C(C(x,y),C(N(N(x)),y))). [hyper(2,a,3180,a,b,4644,a)].
20519 P(C(C(x,N(y)),C(y,N(x)))). [hyper(2,a,71,a,b,19609,a)].
20805 P(C(x,C(C(y,N(x)),N(y)))). [hyper(2,a,3180,a,b,20519,a)].
21589 P(C(N(C(x,y)),C(C(z,N(x)),N(z)))). [hyper(2,a,19593,a,b,20805,a)].
29513 P(C(C(x,N(y)),C(N(C(y,z)),N(x)))). [hyper(2,a,3180,a,b,21589,a)].
29514 $F. [resolve(29513,a,6,a)].

share|cite|improve this answer

answered Jul 23 at 21:29

Doug Spoonwood

7,65012042

add a comment | 

up vote
1
down vote

up vote
1
down vote

Here's a proof of a first-order proof using hyperresolution which correlates to a proof using condensed detachment from the theorem prover written by William McCune at Argonne National Laboratory. Also, instead of using infix notation, it uses prefix notation and letters. (x$rightarrow$y) translates to C(x, y) and $lnot$x translates to N(x):

% -------- Comments from original proof --------
% Proof 1 at 31.95 (+ 11.73) seconds.
% Length of proof is 44.
% Level of proof is 16.
% Maximum clause weight is 24.
% Given clauses 3400.

1 P(C(C(x,N(y)),C(N(C(y,z)),N(x)))) # label(non_clause) # label(goal). [goal].
2 -P(C(x,y)) | -P(x) | P(y). [assumption].
3 P(C(x,C(y,x))). [assumption].
4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))). [assumption].
5 P(C(C(N(x),N(y)),C(y,x))). [assumption].
6 -P(C(C(c1,N(c2)),C(N(C(c2,c3)),N(c1)))). [deny(1)].
7 P(C(x,C(y,C(z,y)))). [hyper(2,a,3,a,b,3,a)].
8 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))). [hyper(2,a,4,a,b,4,a)].
9 P(C(x,C(C(y,C(z,u)),C(C(y,z),C(y,u))))). [hyper(2,a,3,a,b,4,a)].
10 P(C(C(x,y),C(x,x))). [hyper(2,a,4,a,b,3,a)].
11 P(C(C(C(N(x),N(y)),y),C(C(N(x),N(y)),x))). [hyper(2,a,4,a,b,5,a)].
12 P(C(x,C(C(N(y),N(z)),C(z,y)))). [hyper(2,a,3,a,b,5,a)].
14 P(C(x,C(y,C(z,C(u,z))))). [hyper(2,a,3,a,b,7,a)].
17 P(C(x,x)). [hyper(2,a,10,a,b,7,a)].
18 P(C(C(C(x,y),x),C(C(x,y),y))). [hyper(2,a,4,a,b,17,a)].
26 P(C(C(x,C(C(y,x),z)),C(x,z))). [hyper(2,a,8,a,b,7,a)].
44 P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))). [hyper(2,a,8,a,b,14,a)].
48 P(C(C(C(x,C(y,z)),C(C(C(x,y),C(x,z)),u)),C(C(x,C(y,z)),u))). [hyper(2,a,8,a,b,9,a)].
71 P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))). [hyper(2,a,4,a,b,12,a)].
159 P(C(N(x),C(x,y))). [hyper(2,a,26,a,b,12,a)].
160 P(C(C(x,y),C(C(z,x),C(z,y)))). [hyper(2,a,26,a,b,9,a)].
166 P(C(x,C(N(y),C(y,z)))). [hyper(2,a,3,a,b,159,a)].
197 P(C(C(C(N(x),C(x,y)),z),z)). [hyper(2,a,18,a,b,166,a)].
815 P(C(C(C(x,y),z),C(y,z))). [hyper(2,a,44,a,b,160,a)].
835 P(C(x,C(C(C(y,z),u),C(z,u)))). [hyper(2,a,3,a,b,815,a)].
841 P(C(x,C(C(x,y),y))). [hyper(2,a,815,a,b,18,a)].
842 P(C(x,C(C(N(y),N(x)),y))). [hyper(2,a,815,a,b,11,a)].
918 P(C(C(x,y),C(x,C(C(y,z),z)))). [hyper(2,a,160,a,b,841,a)].
1299 P(C(C(x,C(N(y),N(x))),C(x,y))). [hyper(2,a,4,a,b,842,a)].
3180 P(C(C(x,C(y,z)),C(y,C(x,z)))). [hyper(2,a,48,a,b,835,a)].
4594 P(C(N(N(x)),x)). [hyper(2,a,197,a,b,1299,a)].
4644 P(C(N(N(x)),C(C(x,y),y))). [hyper(2,a,918,a,b,4594,a)].
4672 P(C(x,N(N(x)))). [hyper(2,a,5,a,b,4594,a)].
4728 P(C(C(x,y),C(x,N(N(y))))). [hyper(2,a,160,a,b,4672,a)].
7574 P(C(N(x),N(N(C(x,y))))). [hyper(2,a,197,a,b,4728,a)].
7977 P(C(N(C(x,y)),x)). [hyper(2,a,5,a,b,7574,a)].
8000 P(C(N(C(x,y)),C(C(x,z),z))). [hyper(2,a,918,a,b,7977,a)].
19593 P(C(C(x,y),C(N(C(x,z)),y))). [hyper(2,a,3180,a,b,8000,a)].
19609 P(C(C(x,y),C(N(N(x)),y))). [hyper(2,a,3180,a,b,4644,a)].
20519 P(C(C(x,N(y)),C(y,N(x)))). [hyper(2,a,71,a,b,19609,a)].
20805 P(C(x,C(C(y,N(x)),N(y)))). [hyper(2,a,3180,a,b,20519,a)].
21589 P(C(N(C(x,y)),C(C(z,N(x)),N(z)))). [hyper(2,a,19593,a,b,20805,a)].
29513 P(C(C(x,N(y)),C(N(C(y,z)),N(x)))). [hyper(2,a,3180,a,b,21589,a)].
29514 $F. [resolve(29513,a,6,a)].

share|cite|improve this answer

answered Jul 23 at 21:29

Doug Spoonwood

7,65012042

Here's a proof of a first-order proof using hyperresolution which correlates to a proof using condensed detachment from the theorem prover written by William McCune at Argonne National Laboratory. Also, instead of using infix notation, it uses prefix notation and letters. (x$rightarrow$y) translates to C(x, y) and $lnot$x translates to N(x):

% -------- Comments from original proof --------
% Proof 1 at 31.95 (+ 11.73) seconds.
% Length of proof is 44.
% Level of proof is 16.
% Maximum clause weight is 24.
% Given clauses 3400.

1 P(C(C(x,N(y)),C(N(C(y,z)),N(x)))) # label(non_clause) # label(goal). [goal].
2 -P(C(x,y)) | -P(x) | P(y). [assumption].
3 P(C(x,C(y,x))). [assumption].
4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))). [assumption].
5 P(C(C(N(x),N(y)),C(y,x))). [assumption].
6 -P(C(C(c1,N(c2)),C(N(C(c2,c3)),N(c1)))). [deny(1)].
7 P(C(x,C(y,C(z,y)))). [hyper(2,a,3,a,b,3,a)].
8 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))). [hyper(2,a,4,a,b,4,a)].
9 P(C(x,C(C(y,C(z,u)),C(C(y,z),C(y,u))))). [hyper(2,a,3,a,b,4,a)].
10 P(C(C(x,y),C(x,x))). [hyper(2,a,4,a,b,3,a)].
11 P(C(C(C(N(x),N(y)),y),C(C(N(x),N(y)),x))). [hyper(2,a,4,a,b,5,a)].
12 P(C(x,C(C(N(y),N(z)),C(z,y)))). [hyper(2,a,3,a,b,5,a)].
14 P(C(x,C(y,C(z,C(u,z))))). [hyper(2,a,3,a,b,7,a)].
17 P(C(x,x)). [hyper(2,a,10,a,b,7,a)].
18 P(C(C(C(x,y),x),C(C(x,y),y))). [hyper(2,a,4,a,b,17,a)].
26 P(C(C(x,C(C(y,x),z)),C(x,z))). [hyper(2,a,8,a,b,7,a)].
44 P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))). [hyper(2,a,8,a,b,14,a)].
48 P(C(C(C(x,C(y,z)),C(C(C(x,y),C(x,z)),u)),C(C(x,C(y,z)),u))). [hyper(2,a,8,a,b,9,a)].
71 P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))). [hyper(2,a,4,a,b,12,a)].
159 P(C(N(x),C(x,y))). [hyper(2,a,26,a,b,12,a)].
160 P(C(C(x,y),C(C(z,x),C(z,y)))). [hyper(2,a,26,a,b,9,a)].
166 P(C(x,C(N(y),C(y,z)))). [hyper(2,a,3,a,b,159,a)].
197 P(C(C(C(N(x),C(x,y)),z),z)). [hyper(2,a,18,a,b,166,a)].
815 P(C(C(C(x,y),z),C(y,z))). [hyper(2,a,44,a,b,160,a)].
835 P(C(x,C(C(C(y,z),u),C(z,u)))). [hyper(2,a,3,a,b,815,a)].
841 P(C(x,C(C(x,y),y))). [hyper(2,a,815,a,b,18,a)].
842 P(C(x,C(C(N(y),N(x)),y))). [hyper(2,a,815,a,b,11,a)].
918 P(C(C(x,y),C(x,C(C(y,z),z)))). [hyper(2,a,160,a,b,841,a)].
1299 P(C(C(x,C(N(y),N(x))),C(x,y))). [hyper(2,a,4,a,b,842,a)].
3180 P(C(C(x,C(y,z)),C(y,C(x,z)))). [hyper(2,a,48,a,b,835,a)].
4594 P(C(N(N(x)),x)). [hyper(2,a,197,a,b,1299,a)].
4644 P(C(N(N(x)),C(C(x,y),y))). [hyper(2,a,918,a,b,4594,a)].
4672 P(C(x,N(N(x)))). [hyper(2,a,5,a,b,4594,a)].
4728 P(C(C(x,y),C(x,N(N(y))))). [hyper(2,a,160,a,b,4672,a)].
7574 P(C(N(x),N(N(C(x,y))))). [hyper(2,a,197,a,b,4728,a)].
7977 P(C(N(C(x,y)),x)). [hyper(2,a,5,a,b,7574,a)].
8000 P(C(N(C(x,y)),C(C(x,z),z))). [hyper(2,a,918,a,b,7977,a)].
19593 P(C(C(x,y),C(N(C(x,z)),y))). [hyper(2,a,3180,a,b,8000,a)].
19609 P(C(C(x,y),C(N(N(x)),y))). [hyper(2,a,3180,a,b,4644,a)].
20519 P(C(C(x,N(y)),C(y,N(x)))). [hyper(2,a,71,a,b,19609,a)].
20805 P(C(x,C(C(y,N(x)),N(y)))). [hyper(2,a,3180,a,b,20519,a)].
21589 P(C(N(C(x,y)),C(C(z,N(x)),N(z)))). [hyper(2,a,19593,a,b,20805,a)].
29513 P(C(C(x,N(y)),C(N(C(y,z)),N(x)))). [hyper(2,a,3180,a,b,21589,a)].
29514 $F. [resolve(29513,a,6,a)].

share|cite|improve this answer

answered Jul 23 at 21:29

Doug Spoonwood

7,65012042

share|cite|improve this answer

share|cite|improve this answer

answered Jul 23 at 21:29

Doug Spoonwood

7,65012042

answered Jul 23 at 21:29

Doug Spoonwood

7,65012042

answered Jul 23 at 21:29

Doug Spoonwood

7,65012042

7,65012042

add a comment | 

add a comment | 

 

draft saved

draft discarded

 

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

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2860265%2fhow-to-prove-a-rightarrow-negb-rightarrow-negb-rightarrow-c-rightarr%23new-answer', 'question_page');

);

Post as a guest

Name Email

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

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

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

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Name Email

Name

Email

Name Email

Name

Email