Lets take this "truth":

> Quine explains, “No bachelor is married,” where
the 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,” where
> the 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"

Am 02.05.2024 um 02:35 schrieb Mild Shock:
> 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,” where
>> the 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 = Nop

and in the datebase:
father(I, Nobody)
father(Nobody, I)

then clearly

grand_father(I,I)

holds. No?

Am 02.05.2024 um 02:35 schrieb Mild Shock:
> 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,” where
>> the 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?
>
>

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? How would you define it?

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?
>>>
>>>
>>
>

Am 03.05.2024 um 03:46 schrieb Mild Shock:
> 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? [...]

Indeed. A thinko, sorry.

> 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?
>>>>
>>>>
>>>
>>
>