Skip to main content
Mathematica

Return to Answer

Fixed a typo, added links, fixed combinator logic proof
Source Link
Matt W-D
Matt W-D
  • 306
  • 3
  • 7

Pretty cool; EquationalLogic`FindCounterexample is still mysterious (at least to me), but I managed to get it to do something more interesting than spit back numbers.

EquationalLogic`FindCounterexample[f[a, i] == a, f[a, a] == a]
(* {{f -> ({{1, 2}, {1, 1}}[[##1]] &), a -> 1}, {i -> 2}} *)

It appears the the first clause satisfies the logical constraints from the second argument (i.e., the assumptions) and the second clause makes the first clause false.

This is speculation, but perhaps EquationalLogic`FindCounterexample returns a number when it has some kind of error.

EquationalLogic`FindProof and EquationalLogic`Prove appears to be implementing a term-rewriting based proof system (like Equational Logic from Mathworld). This reminds me of SIMP_TAC from the computer proof assistant HOL Light.

A key difference is that the logic of this prover does not follow the following rules from equational logic: $$\frac{a=b}{f(a)=f(b)}$$ $$\frac{a=b}{a(x)=b(x)}$$

Seems to work fine as a term-rewriting prover despite lacking those rules. Here's a little proof in combinatory logic using the EquationalLogic prover:

EquationalLogic`Prove[EquationalLogic`Prove[ForAll[x, ((s@k)@k)@x == x], 
    ForAll[x, Composition[s, k]@k@x == x], 
                ForAll[{x, y}, Composition[k, x]@y(k@x)@y == x] && 
                        ForAll[{f, g, x}, Composition[s, f]@g@x((s@f)@g)@x == Composition[f, g]@Composition[g, x]]
]
(f@x)@(g@x)]]
(* True *)

You can do a lot of this stuff with Prover9, if you want a point of comparison.

As a final note, since it is apparently possible to express combinatory logic in this system, it is possible to ask the EquationalLogic prover to prove an undecidable proposition. From my own experiments, it will eat up all of your memory if you ask it to prove something it can't.

Pretty cool; EquationalLogic`FindCounterexample is still mysterious (at least to me), but I managed to get it to do something more interesting than spit back numbers.

EquationalLogic`FindCounterexample[f[a, i] == a, f[a, a] == a]
(* {{f -> ({{1, 2}, {1, 1}}[[##1]] &), a -> 1}, {i -> 2}} *)

It appears the the first clause satisfies the logical constraints from the second argument (i.e., the assumptions) and the second clause makes the first clause false.

This is speculation, but perhaps EquationalLogic`FindCounterexample returns a number when it has some kind of error.

EquationalLogic`FindProof and EquationalLogic`Prove appears to be implementing a term-rewriting based proof system (like Equational Logic from Mathworld). This reminds me of SIMP_TAC from the computer proof assistant HOL Light.

A key difference is that the logic of this prover does not follow the following rules from equational logic: $$\frac{a=b}{f(a)=f(b)}$$ $$\frac{a=b}{a(x)=b(x)}$$

Seems to work fine as a term-rewriting prover despite lacking those rules. Here's a little proof in combinatory logic using the EquationalLogic prover:

EquationalLogic`Prove[
    ForAll[x, Composition[s, k]@k@x == x], 
     ForAll[{x, y}, Composition[k, x]@y == x] && 
    ForAll[{f, g, x}, Composition[s, f]@g@x == Composition[f, g]@Composition[g, x]]
]

(* True *)

You can do a lot of this stuff with Prover9, if you want a point of comparison.

As a final note, since it is apparently possible to express combinatory logic in this system, it is possible to ask the EquationalLogic prover to prove an undecidable proposition. From my own experiments, it will eat up all of your memory if you ask it to prove something it can't.

Pretty cool; EquationalLogic`FindCounterexample is still mysterious (at least to me), but I managed to get it to do something more interesting than spit back numbers.

EquationalLogic`FindCounterexample[f[a, i] == a, f[a, a] == a]
(* {{f -> ({{1, 2}, {1, 1}}[[##1]] &), a -> 1}, {i -> 2}} *)

It appears the the first clause satisfies the logical constraints from the second argument (i.e., the assumptions) and the second clause makes the first clause false.

This is speculation, but perhaps EquationalLogic`FindCounterexample returns a number when it has some kind of error.

EquationalLogic`FindProof and EquationalLogic`Prove appears to be implementing a term-rewriting based proof system (like Equational Logic from Mathworld). This reminds me of SIMP_TAC from the computer proof assistant HOL Light.

A key difference is that the logic of this prover does not follow the following rules from equational logic: $$\frac{a=b}{f(a)=f(b)}$$ $$\frac{a=b}{a(x)=b(x)}$$

Seems to work fine as a term-rewriting prover despite lacking those rules. Here's a little proof in combinatory logic using the EquationalLogic prover:

EquationalLogic`Prove[ForAll[x, ((s@k)@k)@x == x], 
                        ForAll[{x, y}, (k@x)@y == x] && 
                        ForAll[{f, g, x}, ((s@f)@g)@x == (f@x)@(g@x)]]
(* True *)

You can do a lot of this stuff with Prover9, if you want a point of comparison.

As a final note, since it is apparently possible to express combinatory logic in this system, it is possible to ask the EquationalLogic prover to prove an undecidable proposition. From my own experiments, it will eat up all of your memory if you ask it to prove something it can't.

Fixed a typo, added links
Source Link
Matt W-D
Matt W-D
  • 306
  • 3
  • 7

Pretty cool; EquationalLogic`FindCounterexample is still pretty mysterious (at least to me), but I managed to get it to do something more interesting than spit back numbers.

EquationalLogic`FindCounterexample[f[a, i] == a, f[a, a] == a]
(* {{f -> ({{1, 2}, {1, 1}}[[##1]] &), a -> 1}, {i -> 2}} *)

It appears the the first clause satisfies the logical constraints from the second argument (i.e., the assumptions) and the second clause makes violates the first clause false.

This is speculation, but perhaps EquationalLogic`FindCounterexample returns a number when it has some kind of error.

EquationalLogic`FindProof and EquationalLogic`Prove appears to be implementing a term-rewriting based proof system (like Equational Logic from Mathworld). This reminds me of SIMP_TAC from the computer proof assistant HOL LightHOL Light.

A key difference is that the logic of this prover does not follow the following rules from equational logic: $$\frac{a=b}{f(a)=f(b)}$$ $$\frac{a=b}{a(x)=b(x)}$$

Seems to work fine as a term-rewriting prover despite lacking those rules. Here's a little proof in combinatory logic using the EquationalLogic prover:

EquationalLogic`Prove[
    ForAll[x, Composition[s, k]@k@x == x], 
    ForAll[{x, y}, Composition[k, x]@y == x] && 
    ForAll[{f, g, x}, Composition[s, f]@g@x == Composition[f, g]@Composition[g, x]]
]

(* True *)

You can do a lot of this stuff with Prover9Prover9, if you want a point of comparison.

As a final note, since it is apparently possible to express combinatory logic in this system, it is possible to ask the EquationalLogic prover to prove an undecidable proposition. From my own experiments, it will eat up all of your memory if you ask it to prove something it can't.

Pretty cool; EquationalLogic`FindCounterexample is still pretty mysterious (at least to me), but I managed to get it to do something more interesting than spit back numbers.

EquationalLogic`FindCounterexample[f[a, i] == a, f[a, a] == a]
(* {{f -> ({{1, 2}, {1, 1}}[[##1]] &), a -> 1}, {i -> 2}} *)

It appears the the first clause satisfies the logical constraints from the second argument (i.e., the assumptions) and the second clause makes violates the first clause.

This is speculation, but perhaps EquationalLogic`FindCounterexample returns a number when it has some kind of error.

EquationalLogic`FindProof and EquationalLogic`Prove appears to be implementing a term-rewriting based proof system (like Equational Logic from Mathworld). This reminds me of SIMP_TAC from the computer proof assistant HOL Light.

A key difference is that the logic of this prover does not follow the following rules from equational logic: $$\frac{a=b}{f(a)=f(b)}$$ $$\frac{a=b}{a(x)=b(x)}$$

Seems to work fine as a term-rewriting prover despite lacking those rules. Here's a little proof in combinatory logic using the EquationalLogic prover:

EquationalLogic`Prove[
    ForAll[x, Composition[s, k]@k@x == x], 
    ForAll[{x, y}, Composition[k, x]@y == x] && 
    ForAll[{f, g, x}, Composition[s, f]@g@x == Composition[f, g]@Composition[g, x]]
]

(* True *)

You can do a lot of this stuff with Prover9, if you want a point of comparison.

As a final note, since it is apparently possible to express combinatory logic in this system, it is possible to ask the EquationalLogic prover to prove an undecidable proposition. From my own experiments, it will eat up all of your memory if you ask it to prove something it can't.

Pretty cool; EquationalLogic`FindCounterexample is still mysterious (at least to me), but I managed to get it to do something more interesting than spit back numbers.

EquationalLogic`FindCounterexample[f[a, i] == a, f[a, a] == a]
(* {{f -> ({{1, 2}, {1, 1}}[[##1]] &), a -> 1}, {i -> 2}} *)

It appears the the first clause satisfies the logical constraints from the second argument (i.e., the assumptions) and the second clause makes the first clause false.

This is speculation, but perhaps EquationalLogic`FindCounterexample returns a number when it has some kind of error.

EquationalLogic`FindProof and EquationalLogic`Prove appears to be implementing a term-rewriting based proof system (like Equational Logic from Mathworld). This reminds me of SIMP_TAC from the computer proof assistant HOL Light.

A key difference is that the logic of this prover does not follow the following rules from equational logic: $$\frac{a=b}{f(a)=f(b)}$$ $$\frac{a=b}{a(x)=b(x)}$$

Seems to work fine as a term-rewriting prover despite lacking those rules. Here's a little proof in combinatory logic using the EquationalLogic prover:

EquationalLogic`Prove[
    ForAll[x, Composition[s, k]@k@x == x], 
    ForAll[{x, y}, Composition[k, x]@y == x] && 
    ForAll[{f, g, x}, Composition[s, f]@g@x == Composition[f, g]@Composition[g, x]]
]

(* True *)

You can do a lot of this stuff with Prover9, if you want a point of comparison.

As a final note, since it is apparently possible to express combinatory logic in this system, it is possible to ask the EquationalLogic prover to prove an undecidable proposition. From my own experiments, it will eat up all of your memory if you ask it to prove something it can't.

deleted 43 characters in body
Source Link
rm -rf ♦
rm -rf ♦
  • 89.3k
  • 21
  • 296
  • 478

Pretty cool; EquationalLogic`FindCounterexample is still pretty mysterious (at least to me), but I managed to get it to do something more interesting than spit back numbers.

 In[1]:= EquationalLogic`FindCounterexample[f[a, i] == a, f[a, a] == a]
Out[1]:=(* {{f -> ({{1, 2}, {1, 1}}[[##1]] &), a -> 1}, {i -> 2}} *)

It appears the the first clause satisfies the logical constraints from the second argument (i.e., the assumptions) and the second clause makes violates the first clause.

This is speculation, but perhaps EquationalLogic`FindCounterexample returns a number when it has some kind of error.

EquationalLogic`FindProof and EquationalLogic`Prove appears to be implementing a term-rewriting based proof system (like Equational Logic from Mathworld). This reminds me of SIMP_TAC from the computer proof assistant HOL Light.

A key difference is that the logic of this prover does not follow the following rules from equational logic: $$\frac{a=b}{f(a)=f(b)}$$ $$\frac{a=b}{a(x)=b(x)}$$

Seems to work fine as a term-rewriting prover despite lacking those rules. Here's a little proof in combinatory logic using the EquationalLogic prover (I've used $\LaTeX$ for pretty printing)EquationalLogic prover:

$In[2]:=\text{EquationalLogic$`$Prove}[\forall _x((s\circ k)\circ k)\circ x==x,\forall _{\{x,y\}}(k\circ x)\circ y==x\\\&\&\ \forall _{\{f,g,x\}}((s\circ f)\circ g)\circ x==(f\circ x)\circ (g\circ x)]$

Out[2]EquationalLogic`Prove[
 :=   ForAll[x, Composition[s, k]@k@x == x], 
    ForAll[{x, y}, Composition[k, x]@y == x] && 
    ForAll[{f, g, x}, Composition[s, f]@g@x == Composition[f, g]@Composition[g, x]]
]

(* True *)

You can do a lot of this stuff with Prover9, if you want a point of comparison.

As a final note, since it is apparently possible to express combinatory logic in this system, it is possible to ask the EquationalLogicEquationalLogic prover to prove an undecidable proposition. From my own experiments, it will eat up all of your memory if you ask it to prove something it can't.

Pretty cool; EquationalLogic`FindCounterexample is still pretty mysterious (at least to me), but I managed to get it to do something more interesting than spit back numbers.

 In[1]:= EquationalLogic`FindCounterexample[f[a, i] == a, f[a, a] == a]
Out[1]:= {{f -> ({{1, 2}, {1, 1}}[[##1]] &), a -> 1}, {i -> 2}}

It appears the the first clause satisfies the logical constraints from the second argument (i.e., the assumptions) and the second clause makes violates the first clause.

This is speculation, but perhaps EquationalLogic`FindCounterexample returns a number when it has some kind of error.

EquationalLogic`FindProof and EquationalLogic`Prove appears to be implementing a term-rewriting based proof system (like Equational Logic from Mathworld). This reminds me of SIMP_TAC from the computer proof assistant HOL Light.

A key difference is that the logic of this prover does not follow the following rules from equational logic: $$\frac{a=b}{f(a)=f(b)}$$ $$\frac{a=b}{a(x)=b(x)}$$

Seems to work fine as a term-rewriting prover despite lacking those rules. Here's a little proof in combinatory logic using the EquationalLogic prover (I've used $\LaTeX$ for pretty printing):

$In[2]:=\text{EquationalLogic$`$Prove}[\forall _x((s\circ k)\circ k)\circ x==x,\forall _{\{x,y\}}(k\circ x)\circ y==x\\\&\&\ \forall _{\{f,g,x\}}((s\circ f)\circ g)\circ x==(f\circ x)\circ (g\circ x)]$

Out[2] := True

You can do a lot of this stuff with Prover9, if you want a point of comparison.

As a final note, since it is apparently possible to express combinatory logic in this system, it is possible to ask the EquationalLogic prover to prove an undecidable proposition. From my own experiments, it will eat up all of your memory if you ask it to prove something it can't.

Pretty cool; EquationalLogic`FindCounterexample is still pretty mysterious (at least to me), but I managed to get it to do something more interesting than spit back numbers.

EquationalLogic`FindCounterexample[f[a, i] == a, f[a, a] == a]
(* {{f -> ({{1, 2}, {1, 1}}[[##1]] &), a -> 1}, {i -> 2}} *)

It appears the the first clause satisfies the logical constraints from the second argument (i.e., the assumptions) and the second clause makes violates the first clause.

This is speculation, but perhaps EquationalLogic`FindCounterexample returns a number when it has some kind of error.

EquationalLogic`FindProof and EquationalLogic`Prove appears to be implementing a term-rewriting based proof system (like Equational Logic from Mathworld). This reminds me of SIMP_TAC from the computer proof assistant HOL Light.

A key difference is that the logic of this prover does not follow the following rules from equational logic: $$\frac{a=b}{f(a)=f(b)}$$ $$\frac{a=b}{a(x)=b(x)}$$

Seems to work fine as a term-rewriting prover despite lacking those rules. Here's a little proof in combinatory logic using the EquationalLogic prover:

EquationalLogic`Prove[
    ForAll[x, Composition[s, k]@k@x == x], 
    ForAll[{x, y}, Composition[k, x]@y == x] && 
    ForAll[{f, g, x}, Composition[s, f]@g@x == Composition[f, g]@Composition[g, x]]
]

(* True *)

You can do a lot of this stuff with Prover9, if you want a point of comparison.

As a final note, since it is apparently possible to express combinatory logic in this system, it is possible to ask the EquationalLogic prover to prove an undecidable proposition. From my own experiments, it will eat up all of your memory if you ask it to prove something it can't.

Source Link
Matt W-D
Matt W-D
  • 306
  • 3
  • 7