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"
On 27/04/2024 16:43, Mild Shock wrote:
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"
If you want it to. The additional rule needed is that X can not be an ancestor of X.
--
---------------------------
| BBB b \ Barbara at LivingHistory stop co stop uk
| B B aa rrr b |
| BBB a a r bbb | Quidquid latine dictum sit,
| B B a a r b b | altum videtur.
| BBB aa a r bbb |
-----------------------------
Well I forgot to say, that only first order
logic with equality, FOL=, is available.
How would you define ancestor?
Barb Knox schrieb:
On 27/04/2024 16:43, Mild Shock wrote:
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"
If you want it to. The additional rule needed is that X can not be an
ancestor of X.
--
---------------------------
| BBB b \ Barbara at LivingHistory stop co stop uk
| B B aa rrr b |
| BBB a a r bbb | Quidquid latine dictum sit,
| B B a a r b b | altum videtur.
| BBB aa a r bbb |
-----------------------------
Well I forgot to say, that only first order
logic with equality, FOL=, is available.
How would you define ancestor?
Barb Knox schrieb:---------------------------
On 27/04/2024 16:43, Mild Shock wrote:
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"
If you want it to. The additional rule needed is that X can not be an
ancestor of X.
--
You also forgot that you posed this as a Prolog, not an FOL, problem.
This is beginning to smell a lot like homework.
Its only work if you don't like it, otherwise
its pure logic programming joy. I didn't have
time to try an ancestor formalization yet.
Yes the requirememt is FOL, from the SWI-Prolog
thread one can extract that I am using the
Vidal-Rosset Variant of the Otten Prover Syntax:
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
:- op( 500, fy, !). % universal quantifier: ![X]:
:- op( 500, fy, ?). % existential quantifier: ?[X]:
:- op( 500,xfy, :).
Thats the Operator definitions in Prolog
to feed the Otten Prover with FOL formulas.
I use the same Operators to feed my model
finder with FOL formulas. Now I have rewritten
the model finder to give a better output:
?- counter(1).
father(0,0)-1
grand_father(0,0)-1
true ;
[...]
father(0,0)-0
father(0,1)-1
father(1,0)-1
father(1,1)-0
grand_father(0,0)-1
grand_father(0,1)-0
grand_father(1,0)-0
grand_father(1,1)-1
true
This is the cosmetic makeover of the model finder:
% problem(+Integer, -Formula)
problem(1, (
![X]:![Y]:(?[Z]:(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)) =>
~ ?[X]:grand_father(X,X))).
% counter(+Integer)
counter(K) :-
problem(K, F),
between(1, 3, N),
expand(F, N, G),
quine(G, M, V),
V = 0,
keysort(M, L),
(member(X, L), write(X), nl, fail; true).
Plus expand/3 and quine/3 are found here: https://swi-prolog.discourse.group/t/7398
Barb Knox schrieb:
This is beginning to smell a lot like homework.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 491 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 117:49:58 |
| Calls: | 9,686 |
| Calls today: | 2 |
| Files: | 13,728 |
| Messages: | 6,176,335 |