As you know, NK is very handy to check validity of a formula by pencil and paper. I used it to know validity of a formula before running leanTAP.
Too difficult for me. Instead, now, I asked leanTAP:
% ?- time( prove( ( some(x, -q(x)) -> some(x, q(x))) -> some(x, q(x)))).
%@ % 651 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 7482759 Lips)
I had tested. I remember you gave me. Thanks.
% ?- prove(p).
%@ false.
% ?- prove(all(y, some(x, f(x, y)) -> some(x, all(y, f(x, y))))).
%@ false.
% ?- prove(some(y, all(x, f(x, y)) -> all(x, some(y, f(x, y))))).
%@ true .
I am missing something. If a is taken as a free variable, then
your reconstruction violates eigen variable condition. Also I am not sure whether arity 0 skolem function is allowed to be as a free variable. Skolemization is not in LK. I gave up. I ask teacher
for answer.
I am not sure whether I understand what you are trying to fix, but it seems interesting. However I am afraid that I have only student level of knowledge to help for fixing.
Thanks. I will test soon in the future. It is impressive that you seem to doubt something correctness of leanTAP. As for me, I trusted except using limit of number of variables, and all others are justified under structural rules of LK (exchange, contraction, weakening). But I must check, because I want to put it in my pocket as like a handy calculator. In fact, I tested the famous âRussel setsâ formula and was surprised to see that it took 0.000 seconds !! I donât doubt, but want to check for myself. Until I am convinced to my codes, I will keep silent. Thanks.
I just have tested. For pel38, pl47, overbeek1, overbeek2, and overbeek4, it was âtime_limit_exceeded.â Fortunately, the other test cases in the file were proved. I have no idea how to pass these 4 time_limit_exeeded cases, and it seems beyond my skills. I enjoyed coding, and I like this toy prover. From time time I will play around with my toy codes.
%@ pel38time_limit_exceeded
%@ pel47time_limit_exceeded
%@ overbeek1time_limit_exceeded
%@ overbeek2time_limit_exceeded
%@ overbeek4time_limit_exceeded
I found a comment line in the leantest.pl the uv_incprovfm runs over all problems in the database, which is more than I expected. As the source is available, I will check it. In fact I am doing, though not runs over all yet.
As leanTAP creates skolem functions, it seems difficult to build LK proof figure on leanTAP, because existential quantifiers are dropped off from the input formula like provers in clausal forms, that is, the proof is for some validity equivalent formula to the input one. More direct use of LK system is a right direction. In this respect, if I understand correctly, you are on the right way. But as for me, yes/no/time_limit_exceeded answer is enough like a calculator without showing steps.
EDIT: Only one of the four hard problems, which I could not pass, has been passed. nnf/2 is my version, and time limit was set 60 seconds (too short ?). uv_incprovefml is short like leanTAP, I hope I could read it.
% ?- call_with_time_limit(60, uv_incprovefml(pel47)).
%@ pel47
%@ ERROR: Unhandled exception: Time limit exceeded
% ?- call_with_time_limit(60, uv_incprovefml(overbeek1)).
%@ overbeek1
%@ proved in 33017 msec, found VarLim = 19
%@ true.
% ?- call_with_time_limit(60, uv_incprovefml(overbeek2)).
%@ overbeek2
%@ ERROR: Unhandled exception: Time limit exceeded
% ?- call_with_time_limit(60, uv_incprovefml(overbeek4)).
%@ overbeek4
%@ ERROR: Unhandled exception: Time limit exceeded
This is new to me if this means that some(x, all(y, p(x,y)))
can be converted to some(x, p(x, f(x))) for prover.
What I know is similar but different: all(x, some(y, p(x,y))) can converted to all(x, p(x, f(x))) in the sense of provability. Am I missing ? Or you are talking about new and important thing.
(Nothing of Relevance here)
A set of clauses is viewed as DNF or CNF depending on the purpose, and negation of DNF can be converted to logically equivalent CNF as propositional cases, and vice versa. So I donât think I am confused.
Is Herbrand theorem (1930) is so called completeness of Herbrand interpretation (or Free interpretation), which prologers are familiar with. I guess the choice axiom must be used for that because of Skolem function was used. Skolem symbol is interpreted as a choice function.
The input formulae in the leantest.pl for leanTAP are negated, which, I guess, leanTAP mimics one-sided sequent LK calculus with empty right.
I have not seen nnf preprocesser source yet, but I am almost sure that the nnf introduces Skolem function symbols because in leanTAP no clause is found for existential quantifiers as if no such quantifier appeared in the input.
Thank you for many interesting comments, though I could reply to only a few of them.
But I see in the leantest.pl which you recommended to try,
fml(pel1,0,-((p => q) <=> (-q => -p))).
fml(pel2,0,-(-(-p) <=> p)).
fml(pel3,0,-(-(p => q) => (q => p))).
in which the input formula to be proved seems negated.
Really ? If so, this means skolemization is not necessary. But on the other hand, special cares to be paid to universally quantified variable for the all-right rule. I will check it in the future when I have chance to do. So far, I thought right-empty sequent is much suitable for Prolog in some reasons.
Yes, I am confused. But anyway, following this thread, I have learned interesting stuff, e.g. leanTAP. Now I would like to find a way to pass the remaining last three probelms in the leantest.pl which uv_incprovfml could not pass yet on my computing resource despite of the comment in the file like âyes, you can pass.â I am not sure that I am able to find a way to pass, but
surely it is my pleasure to waste time on that.
Wasât it you that recommended me to try. Perhaps also you didnât try. You should have given me a warning beforehand. But anyway I should thank you because I got a simple pocket calculator for full FOL. It is handy for daily life, not for hard problems.
Here is the output of my prover in the âCompilation Phaseâ where it converts PNF to executable prolog code.
Some of these are trivial ⌠others are notâŚ
Think of
~P as a database you prove Pâs (with current arg binding!) to be false.
P as a database you prove Pâs (with current arg binding!) to be true.l
It covers modus tollens it allows Open World reasoning
% ============================================================
all rooms have a door
============================================================
:- test_boxlog([+assert],all(R,exists(D,implies(room(R),and(door(D),has(R,D)))))).
Should be simular in meaning to
door(D) :-
room(R),
skolem(D, skIsDoorInUnkArg2ofHas_1Fn(R)).
~room(R) :-
\+ (
door(D)
).
~room(R) :-
\+ (
has(R, D)
).
has(R, D) :-
room(R),
skolem(D, skIsDoorInUnkArg2ofHas_1Fn(R)).
============================================================
joe knows all rooms have a door
============================================================
:- test_boxlog(knows(joe,all(R,implies(room(R),exists(D,and(door(D),has(R,D))))))) .
Should be simular in meaning to
~knows(joe, room(A)) :-
\+ (
knows(joe, door(B))
).
~knows(joe, room(A)) :-
\+ (
knows(joe, has(A, B))
).
knows(joe, door(A)) :-
knows(joe, room(B)),
skolem(A, skIsDoorInUnkArg2ofHas_2Fn(B)).
knows(joe, has(A, B)) :-
knows(joe, room(A)),
skolem(B, skIsDoorInUnkArg2ofHas_2Fn(A)).
============================================================
for all rooms joe knows about he belives a door exists
============================================================
:- test_boxlog(all(R,implies(knows(joe,room(R)),belives(joe,exists(D,and(door(D),has(R,D))))))).
~knows(joe, room(A)) :-
\+ (
belives(joe, door(B))
).
~knows(joe, room(A)) :-
\+ (
belives(joe, has(A, B))
).
belives(joe, door(A)) :-
knows(joe, room(B)),
skolem(A, skIsDoorInUnkArg2ofHas_3Fn(B)).
belives(joe, has(A, B)) :-
knows(joe, room(A)),
skolem(B, skIsDoorInUnkArg2ofHas_3Fn(A)).
============================================================
For joe to eat the food it must be possible that the food is food and joe can eat it
============================================================
:- test_boxlog(poss(&(eats(joe,X),food(X)))=>(eats(joe,X),food(X))).
eats(joe,X) :-
\+ ~eats(joe,X),
\+ ~food(X).
food(X) :-
\+ ~eats(joe,X),
\+ ~food(X).
============================================================================================
Organized Groups of prolog programmers have prolog programmers as members
============================================================================================
:- test_boxlog(implies(and(instance(M,tGroupedPrologOrganization),hasMembers(M,A)), instance(A,tClazzPrologPerson))).
~hasMembers(_11164,_11142):- \+ (instance(_11164,tGroupedPrologOrganization),instance(_11142,tClazzPrologPerson)).
~instance(_11540,tGroupedPrologOrganization):- \+ (hasMembers(_11540,_11518),instance(_11518,tClazzPrologPerson)).
instance(_11874,tClazzPrologPerson):-instance(_11896,tGroupedPrologOrganization),hasMembers(_11896,_11874).
============================================================================================
Those competeing in watersports may not wear shoes
============================================================================================
:- test_boxlog( =>(instance(ATH,tAgent),implies(and(instance(COMP,actAquaticSportsEvent),
competingAgents(COMP,ATH)),holdsIn(COMP,all(CLOTHING,not(and(instance(CLOTHING,tObjectShoe),wearsClothing(ATH,CLOTHING)))))))).
/*
Bad
~competingAgents(_20514,_20492):- ~holdsIn(_20514,v(~instance(_20470,tObjectShoe),~wearsClothing(_20492,_20470))),instance(_20514,actAquaticSportsEvent),instance(_20492,tAgent)
~instance(_20902,tAgent):- ~holdsIn(_20858,v(~instance(_20880,tObjectShoe),~wearsClothing(_20902,_20880))),instance(_20858,actAquaticSportsEvent),competingAgents(_20858,_20902)
~instance(_21272,actAquaticSportsEvent):- ~holdsIn(_21272,v(~instance(_21250,tObjectShoe),~wearsClothing(_21228,_21250))),competingAgents(_21272,_21228),instance(_21228,tAgent)
holdsIn(_21612,v(~instance(_21634,tObjectShoe),~wearsClothing(_21590,_21634))):-instance(_21612,actAquaticSportsEvent),competingAgents(_21612,_21590),instance(_21590,tAgent)
*/
% Good !!!
~occuring(COMP) :-
instance(ATH, tAgent),
instance(COMP, actAquaticSportsEvent),
competingAgents(COMP, ATH),
instance(CLOTHING, tObjectShoe),
wearsClothing(ATH, CLOTHING).
~competingAgents(COMP, ATH) :-
instance(ATH, tAgent),
instance(COMP, actAquaticSportsEvent),
occuring(COMP),
instance(CLOTHING, tObjectShoe),
wearsClothing(ATH, CLOTHING).
~instance(CLOTHING, tObjectShoe) :-
instance(ATH, tAgent),
instance(COMP, actAquaticSportsEvent),
competingAgents(COMP, ATH),
occuring(COMP),
wearsClothing(ATH, CLOTHING).
~instance(COMP, actAquaticSportsEvent) :-
instance(ATH, tAgent),
competingAgents(COMP, ATH),
occuring(COMP),
instance(CLOTHING, tObjectShoe),
wearsClothing(ATH, CLOTHING).
~instance(ATH, tAgent) :-
instance(COMP, actAquaticSportsEvent),
competingAgents(COMP, ATH),
occuring(COMP),
instance(CLOTHING, tObjectShoe),
wearsClothing(ATH, CLOTHING).
~wearsClothing(ATH, CLOTHING) :-
instance(ATH, tAgent),
instance(COMP, actAquaticSportsEvent),
competingAgents(COMP, ATH),
occuring(COMP),
instance(CLOTHING, tObjectShoe).
================================================================================================================
When sightgseeing is occuring .. there is a tourist present
================================================================================================================
:- test_boxlog(implies(and(instance(Act,actSightseeing),performedBy(Person,Act)),holdsIn(Act,instance(Person,mobTourist)))).
/* OLD
~instance(_11704,actSightseeing):- \+ (performedBy(_11704,_11682),holdsIn(_11704,instance(_11682,mobTourist)))
~performedBy(_12092,_12070):- \+ (instance(_12092,actSightseeing),holdsIn(_12092,instance(_12070,mobTourist)))
holdsIn(_12442,instance(_12420,mobTourist)):-instance(_12442,actSightseeing),performedBy(_12442,_12420)
*/
~occuring(Act) :-
\+ ( instance(Act, actSightseeing),
naf(~performedBy(Person, Act)),
instance(Y, mobTourist)
).
~instance(Act, actSightseeing) :-
\+ ( performedBy(Person, Act),
naf(~occuring(Act)),
instance(Y, mobTourist)
).
~performedBy(Person, Act) :-
\+ ( instance(Act, actSightseeing),
naf(~occuring(Act)),
instance(Y, mobTourist)
).
instance(Y, mobTourist) :-
instance(Act, actSightseeing),
performedBy(Person, Act),
occuring(Act).
================================================================================================================
All rooms have a door (Odd syntax issue)
================================================================================================================
:- test_boxlog(all(R,room(R) => exists(D, and([door(D) , has(R,D)])))).
door(D) :-
room(R),
skolem(D, skIsDoorInUnkArg2ofHas_2Fn(R)),
\+ ~has(R, D).
~room(R) :-
\+ ( has(R, D),
door(D)
).
has(R, D) :-
room(R),
skolem(D, skIsDoorInUnkArg2ofHas_2Fn(R)),
\+ ~door(D).
================================================================================================================
No one whom pays taxes in North america can be a dependant of another in the same year
================================================================================================================
:- set_prolog_flag(runtime_breaks,3).
:- test_boxlog([-ensure,-sort],
or(
holdsIn(YEAR, instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica))),
holdsIn(YEAR, instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada))),
holdsIn(YEAR, instance(PERSON, nartR(mobTaxResidentsFn, iMexico))),
holdsIn(YEAR, instance(PERSON, nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica))),
forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, _SUPPORTEE)))).
~occuring(YEAR) :-
~instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica)),
~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada)),
\+ ( ( forbiddenToDoWrt(iCW_USIncomeTax,
SUPPORTER,
claimsAsDependent(YEAR, SUPPORTER, SUPPORTEE)),
instance(PERSON,
nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica))
),
instance(PERSON, nartR(mobTaxResidentsFn, iMexico))
).
instance(PERSON, nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica)) :-
occuring(YEAR),
~instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica)),
~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada)),
~instance(PERSON, nartR(mobTaxResidentsFn, iMexico)),
\+ ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, SUPPORTEE)).
instance(PERSON, nartR(mobTaxResidentsFn, iMexico)) :-
occuring(YEAR),
~instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica)),
~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada)),
~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica)),
\+ ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, SUPPORTEE)).
instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada)) :-
occuring(YEAR),
~instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica)),
~instance(PERSON, nartR(mobTaxResidentsFn, iMexico)),
~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica)),
\+ ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, SUPPORTEE)).
instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica)) :-
occuring(YEAR),
~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada)),
~instance(PERSON, nartR(mobTaxResidentsFn, iMexico)),
~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica)),
\+ ~forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, SUPPORTEE)).
forbiddenToDoWrt(iCW_USIncomeTax, SUPPORTER, claimsAsDependent(YEAR, SUPPORTER, SUPPORTEE)) :-
occuring(YEAR),
~instance(PERSON, nartR(tClazzCitizenFn, iGroup_UnitedStatesOfAmerica)),
~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_Canada)),
~instance(PERSON, nartR(mobTaxResidentsFn, iMexico)),
\+ ~instance(PERSON, nartR(mobTaxResidentsFn, iGroup_UnitedStatesOfAmerica)).
================================================================================================================
Everything is human or god
================================================================================================================
:- test_boxlog(human(X) v god(X)).
human(_19658) :-
~god(_19658).
god(_23530) :-
~human(_23530).
% ================================================================================================================
% Everything that is human is possibly male
% ================================================================================================================
:- test_boxlog(human(X) => poss(male(X))).
~(human(X)) :-
~poss_t(male, X).
proven_tru(poss_t(male, X)) :-
human(X).
human(_21936). male(_24006).
% ================================================================================================================
% Everything is human and male
% ================================================================================================================
% BAD!! these need co-mingled!
:- test_boxlog((human(X) & male(X))).
=======
Co-mingled!
=======
:- P= (human(X) & male(X)) ,test_boxlog(poss(P) => P).
human(X) :-
\+ ~human(X),
\+ ~male(X).
male(X) :-
\+ ~human(X),
\+ ~male(X).
% These to?
~human(A) :-
\+ ( \+ ~male(A),
human(A)
).
~human(A) :-
\+ ( \+ ~male(A),
male(A)
).
~male(A) :-
\+ ( \+ ~human(A),
human(A)
).
~male(A) :-
\+ ( \+ ~human(A),
male(A)
).
% ================================================================================================================
% Nothing is both human and god
% ================================================================================================================
:- test_boxlog(~ (human(X) & god(X))).
% prolog code results:
~human(_830) :-
god(_830).
~god(_904) :-
human(_904).
% prolog code results:
% ================================================================================================================
% There exists something not evil
% ================================================================================================================
:- test_boxlog(exists(X,~evil(X))).
% prolog code results:
~evil(_788{sk = ...}) :-
skolem(_788{sk = ...}, skIsIn_8Fn).
% prolog code results:
% ================================================================================================================
% There exists something evil
% ================================================================================================================
:- test_boxlog(exists(X,evil(X))).
% prolog code results:
evil(_788{sk = ...}) :-
skolem(_788{sk = ...}, skIsIn_9Fn).
================================================================================================================
When a man exists there will be a god
================================================================================================================
:- test_boxlog(exists(X,man(X)) => exists(G,god(G))).
% prolog code results:
god(_866{sk = ...}) :-
man(_1082),
skolem(_866{sk = ...}, skIsGodIn_1Fn(_1082)).
~man(_2276) :-
\+ ( skolem(_896{sk = ...}, skIsGodIn_1Fn(_2276)),
god(_896{sk = ...})
).
% this would be better though if ?
god(_866{sk = ...}) :-
\= \+ (man(_1082)),
skolem(_866{sk = ...}, skIsGodIn_1Fn).
~man(_2276) :-
\+ god(_896).
% ================================================================================================================
% When two men exists there will be a god
% ================================================================================================================
:- test_boxlog(atleast(2,X,man(X))=>exists(G,god(G))).
god(_1298{sk = ...}) :-
skolem(_1358{sk = ...}, skIsManIn_1Fn(_10978, _1298{sk = ...})),
~man(_1358{sk = ...}),
skolem(_1298{sk = ...}, skIsGodIn_2Fn(_10978)).
god(_3110{sk = ...}) :-
man(_11144),
man(_11166),
skolem(_3110{sk = ...}, skIsGodIn_2Fn(_11166)).
man(_2204{sk = ...}) :-
skolem(_2204{sk = ...}, skIsManIn_1Fn(_11314, _2224{sk = ...})),
skolem(_2224{sk = ...}, skIsGodIn_2Fn(_11314)),
\+ ~god(_2224{sk = ...}).
~man(_11494) :-
\+ ( man(_11516),
naf(~skolem(_4090{sk = ...}, skIsGodIn_2Fn(_11494))),
god(_4090{sk = ...})
).
~man(_11656) :-
\+ ( man(_11678),
naf(~skolem(_4504{sk = ...}, skIsGodIn_2Fn(_11678))),
god(_4504{sk = ...})
).
OR?
god(G) :-
skolem(_1316_sk, skIsManIn_1Fn(X, G)),
~man(_1316_sk),
skolem(G, skIsGodIn_1Fn(X)).
god(G) :-
man(_2720),
~equals(_2742, X),
man(X),
skolem(G, skIsGodIn_1Fn(X)).
man(_1342_sk) :-
skolem(_1342_sk, skIsManIn_1Fn(X, G)),
skolem(G, skIsGodIn_1Fn(X)),
\+ ~god(G).
naf(~equals(_3108, X)) :-
man(_3148),
man(X),
skolem(G, skIsGodIn_1Fn(X)),
\+ ~god(G).
~man(X) :-
man(_3330),
\+ ( \+ ~ (~equals(_3352, X)),
naf(~skolem(G, skIsGodIn_1Fn(X))),
god(G)
).
~man(_3544) :-
~equals(_3566, X),
\+ ( man(X),
naf(~skolem(G, skIsGodIn_1Fn(X))),
god(G)
).
~equals(_1478_sk, X) :-
\+ ( skolem(G, skIsGodIn_1Fn(X)),
god(G)
).
% ================================================================================================================
% A person holding a bird is performing bird holding
% ================================================================================================================
:- test_boxlog([+assert],implies(
and(instance(HOLD, actHoldingAnObject), objectActedOn(HOLD, BIRD), instance(BIRD, tClazzBird),
performedBy(HOLD, PER), instance(PER, mobPerson)),
holdsIn(HOLD, onPhysical(BIRD, PER)))).
% prolog code results:
~occuring(_2056) :-
instance(_2056, actHoldingAnObject),
objectActedOn(_2056, _2078),
instance(_2078, tClazzBird),
\+ ( performedBy(_2056, _2100),
naf(~instance(_2100, mobPerson)),
onPhysical(_2078, _2100)
).
~instance(_2260, mobPerson) :-
instance(_2282, actHoldingAnObject),
objectActedOn(_2282, _2304),
instance(_2304, tClazzBird),
\+ ( performedBy(_2282, _2260),
naf(~occuring(_2282)),
onPhysical(_2304, _2260)
).
~instance(_2520, tClazzBird) :-
instance(_2542, actHoldingAnObject),
objectActedOn(_2542, _2520),
performedBy(_2542, _2564),
\+ ( instance(_2564, mobPerson),
naf(~occuring(_2542)),
onPhysical(_2520, _2564)
).
~instance(_2752, actHoldingAnObject) :-
objectActedOn(_2752, _2774),
instance(_2774, tClazzBird),
performedBy(_2752, _2796),
\+ ( instance(_2796, mobPerson),
naf(~occuring(_2752)),
onPhysical(_2774, _2796)
).
~objectActedOn(_2984, _3006) :-
instance(_2984, actHoldingAnObject),
instance(_3006, tClazzBird),
performedBy(_2984, _3028),
\+ ( instance(_3028, mobPerson),
naf(~occuring(_2984)),
onPhysical(_3006, _3028)
).
~performedBy(_3190, _3212) :-
instance(_3190, actHoldingAnObject),
objectActedOn(_3190, _3234),
instance(_3234, tClazzBird),
\+ ( instance(_3212, mobPerson),
naf(~occuring(_3190)),
onPhysical(_3234, _3212)
).
onPhysical(_3396, _3418) :-
instance(_3440, actHoldingAnObject),
objectActedOn(_3440, _3396),
instance(_3396, tClazzBird),
performedBy(_3440, _3418),
instance(_3418, mobPerson),
occuring(_3440).
I based on Ottsenâs leanTap, Stickelâs PTTP and ROKâs clausify/2
But I see pel47 in the leantest.pl, though I lost already challenge mind for pel47. Also I could not pass pel46. All others in pel series 1-45 are passed in second total.
fml(pel47,44,((-(ex(X1,ex(Y1,(animal(X1) & animal(Y1) & ex(Z1,(isagrain(Z1) & likestoeat(Y1,Z1)) & likestoeat(X1,Y1)))))))
& all(X2,(wolf(X2) => animal(X2))) & ex(X3,wolf(X3))
& all(X4,(fox(X4) => animal(X4))) & ex(X5,fox(X5))
& all(X6,(bird(X6) => animal(X6))) & ex(X7,bird(X7))
& all(X8,(caterpillar(X8) => animal(X8))) & ex(X9,caterpillar(X9))
& all(X10,(snail(X10) => animal(X10))) & ex(X11,snail(X11))
& ex(X12,isagrain(X12)) & all(X13,(isagrain(X13) => isaplant(X13)))
& all(X14,(animal(X14) => (all(Y2,isaplant(Y2) => likestoeat(X14,Y2)) ;
all(Y3,((animal(Y3) & smaller(Y3,X14) & ex(Z1,(isaplant(Z1) & likestoeat(Y3,Z1)))) =>
likestoeat(X14,Y3))))))
& all(X15,all(Y4,((bird(Y4) & (snail(X15) ; caterpillar(X15))) => smaller(X15,Y4))))
& all(X16,all(Y5,((bird(X16) & fox(Y5)) => smaller(X16,Y5))))
& all(X17,all(Y6,((fox(X17) & wolf(Y6)) => smaller(X17,Y6))))
& all(X18,all(Y7,((wolf(X18) & (fox(Y7) ; isagrain(Y7))) => -likestoeat(X18,Y7))))
& all(X19,all(Y8,((bird(X19) & caterpillar(Y8)) => likestoeat(X19,Y8))))
& all(X20,all(Y9,((bird(X20) & snail(Y9)) => -likestoeat(X20,Y9))))
& all(X21,((caterpillar(X21) ; snail(X21)) => ex(Y10,(isaplant(Y10) & likestoeat(X21,Y10)))))
)).
I have passed all pel1-pel46. I had modified leantap for âmanualâ bounded depth first search for fun, though I guess it is not relivant as for the pel series.
% ?- bfs_provefml(_), fail.
%@ pel1 proved in 0 msec, found VarLim = 0
%@ pel2 proved in 0 msec, found VarLim = 0
%@ pel3 proved in 0 msec, found VarLim = 0
%@ pel4 proved in 0 msec, found VarLim = 0
%@ pel5 proved in 0 msec, found VarLim = 0
%@ pel6 proved in 0 msec, found VarLim = 0
%@ pel7 proved in 0 msec, found VarLim = 0
%@ pel8 proved in 0 msec, found VarLim = 0
%@ pel9 proved in 0 msec, found VarLim = 0
%@ pel10 proved in 0 msec, found VarLim = 0
%@ pel11 proved in 0 msec, found VarLim = 0
%@ pel12 proved in 0 msec, found VarLim = 0
%@ pel13 proved in 0 msec, found VarLim = 0
%@ pel14 proved in 0 msec, found VarLim = 0
%@ pel15 proved in 0 msec, found VarLim = 0
%@ pel16 proved in 0 msec, found VarLim = 0
%@ pel17 proved in 1 msec, found VarLim = 0
%@ pel18 proved in 0 msec, found VarLim = 2
%@ pel19 proved in 0 msec, found VarLim = 2
%@ pel20 proved in 0 msec, found VarLim = 6
%@ pel21 proved in 0 msec, found VarLim = 2
%@ pel22 proved in 0 msec, found VarLim = 2
%@ pel23 proved in 0 msec, found VarLim = 1
%@ pel24 proved in 1 msec, found VarLim = 6
%@ pel25 proved in 0 msec, found VarLim = 3
%@ pel26 proved in 0 msec, found VarLim = 3
%@ pel27 proved in 0 msec, found VarLim = 4
%@ pel28 proved in 0 msec, found VarLim = 3
%@ pel29 proved in 1 msec, found VarLim = 10
%@ pel30 proved in 0 msec, found VarLim = 2
%@ pel31 proved in 0 msec, found VarLim = 3
%@ pel32 proved in 0 msec, found VarLim = 3
%@ pel33 proved in 1 msec, found VarLim = 1
%@ pel34 proved in 4 msec, found VarLim = 5
%@ pel35 proved in 0 msec, found VarLim = 4
%@ pel36 proved in 0 msec, found VarLim = 6
%@ pel37 proved in 0 msec, found VarLim = 7
%@ pel38 proved in 4 msec, found VarLim = 4
%@ pel39 proved in 0 msec, found VarLim = 1
%@ pel40 proved in 0 msec, found VarLim = 3
%@ pel41 proved in 0 msec, found VarLim = 3
%@ pel42 proved in 0 msec, found VarLim = 10
%@ pel43 proved in 0 msec, found VarLim = 5
%@ pel44 proved in 0 msec, found VarLim = 3
%@ pel45 proved in 0 msec, found VarLim = 5
%@ pel46 proved in 0 msec, found VarLim = 44
I have checked that result is the same for the original leanTAP source and leantest data. I might have confused pel46 with pel47, just taking wrongly that pel46 did not pass. No problem with pel46 as you said.
I used provefml/1 for the log, which is in the leantest as it is.
As I could not find the nnf and unify source, I defined the two as follow.
nnf(X, Y):- negation_normal_form(X, Y).
unify(X, Y) :- unify_with_occurs_check(X, Y).
negation_normal_form is mine, and I am not sure that It is the same as the original nnf.
% provefml(Name)
% calls fml(Name,Limit,Fml) and tries to prove Fml with VarLim = Limit.
%
% use 'provefml(_),fail.' to prove all formulae in the database
% ?- provefml(_), fail.
% ?- call_with_time_limit(60, (provefml(_), fail)).
provefml(Name) :-
fml(Name,Limit,F),
write(Name),
nnf(F,NNF),
statistics(runtime,[_,_]),
(prove(NNF,Limit)
-> (statistics(runtime,[_,Time]),
format(' proved in ~w msec, VarLim = ~w ~n',[Time,Limit]))
; (statistics(runtime,[_,Time]),
format(' no proof after ~w msec. ~n',[Time]))).
My purpose was to post only that all pel1-pel46 could be passed which is important for me no matter how much time was needed.
BTW, following suggested codes, I tried, but it did not work at all. I am missing something. It takes time for me. As you must keep the original codes of the leantest.pl, it might be much better
for you to test yourself.
ya_provefml(Name):-
fml(Name,Limit,F),
write(Name),
statistics(runtime,[_,_]),
((between(1,1000,_), once(nnf(F,NNF)), once(prove(NNF,Limit)), fail; true)).