Quine explains, “No bachelor is married,” wherethe meaning of the word ‘bachelor’ is synonymous
Lets take this "truth":
Quine explains, “No bachelor is married,” wherethe meaning of the word ‘bachelor’ is synonymous
with the meaning of the word ‘unmarried.’ However,
we can make this kind of analytic claim into a
logical truth (as defined above) by replacing
‘bachelor’ with its synonym, that is, ‘unmarried man,’
to get “No unmarried man is married,” which is an
instance of No not-X is X.
Then examine this "truth":
Lets say you build a Prolog family database and
make definitions for father, grand-father etc..
Will this Prolog family database exclude:
"Im my own grandpa"
Hi,
A full version that has operator definitions
that also work for Scryer Prolog and that uses a
Quine algorithm that even supports function
symbols like in Mace4 by McCune, is found
here on SWI-Prolog SWISH:
McCunes Mace4 Model Finder
https://swish.swi-prolog.org/p/mace4.swinb
Have Fun!
Mild Shock schrieb:
Lets take this "truth":
Quine explains, “No bachelor is married,” wherethe meaning of the word ‘bachelor’ is synonymous
with the meaning of the word ‘unmarried.’ However,
we can make this kind of analytic claim into a
logical truth (as defined above) by replacing
‘bachelor’ with its synonym, that is, ‘unmarried man,’
to get “No unmarried man is married,” which is an
instance of No not-X is X.
Then examine this "truth":
Lets say you build a Prolog family database and
make definitions for father, grand-father etc..
Will this Prolog family database exclude:
"Im my own grandpa"
Hi,
A full version that has operator definitions
that also work for Scryer Prolog and that uses a
Quine algorithm that even supports function
symbols like in Mace4 by McCune, is found
here on SWI-Prolog SWISH:
McCunes Mace4 Model Finder
https://swish.swi-prolog.org/p/mace4.swinb
Have Fun!
Mild Shock schrieb:
Lets take this "truth":
Quine explains, “No bachelor is married,” wherethe meaning of the word ‘bachelor’ is synonymous
with the meaning of the word ‘unmarried.’ However,
we can make this kind of analytic claim into a
logical truth (as defined above) by replacing
‘bachelor’ with its synonym, that is, ‘unmarried man,’
to get “No unmarried man is married,” which is an
instance of No not-X is X.
Then examine this "truth":
Lets say you build a Prolog family database and
make definitions for father, grand-father etc..
Will this Prolog family database exclude:
"Im my own grandpa"
"Problem 1: I am my own grandpa?
Is this possible from terminological definition:
grand_father(X,Y) :- father(X,Z), father(Z,Y)."
Of course. Where's the problem?
If X = Y = I
and Z = Nobody
and in the datebase:
father(I, Nobody)
father(Nobody, I)
then clearly
grand_father(I,I)
holds. No?
Yeah you find such a solution also among
the answers that the model finder generates:
% ?- counter(1).
% father(0,0)-1
% grand_father(0,0)-1
% 1true
% father(0,0)-1 father(0,1)-0 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-0 grand_father(1,1)-0
% 2true
% father(0,0)-1 father(0,1)-1 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-1
grand_father(1,0)-0 grand_father(1,1)-0
% 3true
% father(0,0)-1 father(0,1)-0 father(1,0)-1 father(1,1)-0
grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-1 grand_father(1,1)-0
% 4true
https://swish.swi-prolog.org/p/mace4.swinb
The first solution, is from a domain with size N=1,
and it basically says a counter model is when
there is an individual 0, which is its own father.
The fourth solution, is from a domain with size N=2,
and it basically says a counter model is when
there are two individuals 0 and 1, which are each others father.
Problem 1 is defined as:
/* I am my own grandpa? */
problem(1, (
@[X]: @[Y]:(#[Z]:(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)) =>
~ #[X]:grand_father(X,X))).
I have also toyed around with Problem 2:
/* Is every monoid commutative? */
problem(2, (
(@[X]:(0*X = X) &
@[X]:(X*0 = X) &
@[X]: @[Y]: @[Z]:((X*Y)*Z = X*(Y*Z))) => (a*b = b*a))).
But Problem 3 is quite hard, takes 12 minutes:
/* Is every group commutative? */
problem(3, (
(@[X]:(0*X = X) &
@[X]:(i(X)*X = 0) &
@[X]: @[Y]: @[Z]:((X*Y)*Z = X*(Y*Z))) => (a*b = b*a))).
McCune claims it takes < 1 second with his mace4.
Don't know yet how to speed up Problem 3.
Moebius schrieb:
"Problem 1: I am my own grandpa?
Is this possible from terminological definition:
grand_father(X,Y) :- father(X,Z), father(Z,Y)."
Of course. Where's the problem?
If X = Y = I
and Z = Nobody
and in the datebase:
father(I, Nobody)
father(Nobody, I)
then clearly
grand_father(I,I)
holds. No?
father(I, X_1)
father(X_1, X_2)
:
father(X_n, I)
Am 02.05.2024 um 02:59 schrieb Mild Shock:
Ok, I have to admit that I unconsciously assumed that the database does
not allow for father(a,a) entries. Hence I missed the solutions with
domain size = 1, sorry.
Of course if this restriction does not exist, there's a solution with database entry father(I,I) too. :-)
In general we get a solution (for all n e IN) with database entries
father(I, X_1)
father(X_1, X_2)
:
father(X_n, I)
and I, X_1, ... X_n pairwise distinct.
In this cases: grand_father(I,I) [with domain size = n+1].
Yeah you find such a solution also among
the answers that the model finder generates:
% ?- counter(1).
% father(0,0)-1
% grand_father(0,0)-1
% 1true
% father(0,0)-1 father(0,1)-0 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-0 grand_father(1,1)-0
% 2true
% father(0,0)-1 father(0,1)-1 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-1
grand_father(1,0)-0 grand_father(1,1)-0
% 3true
% father(0,0)-1 father(0,1)-0 father(1,0)-1 father(1,1)-0
grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-1 grand_father(1,1)-0
% 4true
https://swish.swi-prolog.org/p/mace4.swinb
The first solution, is from a domain with size N=1,
and it basically says a counter model is when
there is an individual 0, which is its own father.
The fourth solution, is from a domain with size N=2,
and it basically says a counter model is when
there are two individuals 0 and 1, which are each others father.
Problem 1 is defined as:
/* I am my own grandpa? */
problem(1, (
@[X]: @[Y]:(#[Z]:(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)) => >> ~ #[X]:grand_father(X,X))).
I have also toyed around with Problem 2:
/* Is every monoid commutative? */
problem(2, (
(@[X]:(0*X = X) &
@[X]:(X*0 = X) &
@[X]: @[Y]: @[Z]:((X*Y)*Z = X*(Y*Z))) => (a*b = b*a))).
But Problem 3 is quite hard, takes 12 minutes:
/* Is every group commutative? */
problem(3, (
(@[X]:(0*X = X) &
@[X]:(i(X)*X = 0) &
@[X]: @[Y]: @[Z]:((X*Y)*Z = X*(Y*Z))) => (a*b = b*a))).
McCune claims it takes < 1 second with his mace4.
Don't know yet how to speed up Problem 3.
Moebius schrieb:
"Problem 1: I am my own grandpa?
Is this possible from terminological definition:
grand_father(X,Y) :- father(X,Z), father(Z,Y)."
Of course. Where's the problem?
If X = Y = I
and Z = Nobody
and in the datebase:
father(I, Nobody)
father(Nobody, I)
then clearly
grand_father(I,I)
holds. No?
If the X_i are distinct from each other and distinct from I.
father(I, X_1)
father(X_1, X_2)
:
father(X_n, I)
Its quite difficult to satisfy for n>1:
grand_father(X,Y) :- father(X,Z), father(Z,Y).
Maybe you have ancestor/2 in mind? [...]
Moebius schrieb:
Am 02.05.2024 um 02:59 schrieb Mild Shock:
Ok, I have to admit that I unconsciously assumed that the database
does not allow for father(a,a) entries. Hence I missed the solutions
with domain size = 1, sorry.
Of course if this restriction does not exist, there's a solution with
database entry father(I,I) too. :-)
In general we get a solution (for all n e IN) with database entries
father(I, X_1)
father(X_1, X_2)
:
father(X_n, I)
and I, X_1, ... X_n pairwise distinct.
In this cases: grand_father(I,I) [with domain size = n+1].
Yeah you find such a solution also among
the answers that the model finder generates:
% ?- counter(1).
% father(0,0)-1
% grand_father(0,0)-1
% 1true
% father(0,0)-1 father(0,1)-0 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-0 grand_father(1,1)-0
% 2true
% father(0,0)-1 father(0,1)-1 father(1,0)-0 father(1,1)-0
% grand_father(0,0)-1 grand_father(0,1)-1
grand_father(1,0)-0 grand_father(1,1)-0
% 3true
% father(0,0)-1 father(0,1)-0 father(1,0)-1 father(1,1)-0
grand_father(0,0)-1 grand_father(0,1)-0
grand_father(1,0)-1 grand_father(1,1)-0
% 4true
https://swish.swi-prolog.org/p/mace4.swinb
The first solution, is from a domain with size N=1,
and it basically says a counter model is when
there is an individual 0, which is its own father.
The fourth solution, is from a domain with size N=2,
and it basically says a counter model is when
there are two individuals 0 and 1, which are each others father.
Problem 1 is defined as:
/* I am my own grandpa? */
problem(1, (
@[X]: @[Y]:(#[Z]:(father(X,Z) & father(Z,Y)) <=>
grand_father(X,Y)) =>
~ #[X]:grand_father(X,X))).
I have also toyed around with Problem 2:
/* Is every monoid commutative? */
problem(2, (
(@[X]:(0*X = X) &
@[X]:(X*0 = X) &
@[X]: @[Y]: @[Z]:((X*Y)*Z = X*(Y*Z))) => (a*b = b*a))).
But Problem 3 is quite hard, takes 12 minutes:
/* Is every group commutative? */
problem(3, (
(@[X]:(0*X = X) &
@[X]:(i(X)*X = 0) &
@[X]: @[Y]: @[Z]:((X*Y)*Z = X*(Y*Z))) => (a*b = b*a))).
McCune claims it takes < 1 second with his mace4.
Don't know yet how to speed up Problem 3.
Moebius schrieb:
"Problem 1: I am my own grandpa?
Is this possible from terminological definition:
grand_father(X,Y) :- father(X,Z), father(Z,Y)."
Of course. Where's the problem?
If X = Y = I
and Z = Nobody
and in the datebase:
father(I, Nobody)
father(Nobody, I)
then clearly
grand_father(I,I)
holds. No?
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 307 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 95:23:46 |
| Calls: | 6,849 |
| Files: | 12,352 |
| Messages: | 5,414,877 |