search

leoprover / Leo-III

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
BSD 3-Clause "New" or "Revised" License
42 stars 10 forks source link

Error running Leo-III on SUMO.thf #71

Closed apease closed 2 years ago

apease commented 2 years ago

I tried running Leo-III on the latest SUMO, using output from Sigma's THF translator (written by Christoph). I'm getting

apease@apease-ThinkPad-L14-Gen-1:~/workspace/Leo-III/Leo-III-1.6$ bin/leo3 /home/apease/.sigmakee/KBs/SUMO.thf -t 60 -p % [INFO] Parsing problem /home/apease/.sigmakee/KBs/SUMO.thf ... % OUT OF CHEESE ERROR +++ MELON MELON MELON +++ REDO FROM START % SZS status SyntaxError for /home/apease/.sigmakee/KBs/SUMO.thf : Parse error in file '/home /apease/.sigmakee/KBs/SUMO.thf' in line 1692:309. Unrecognized thf formula input 'APP'

But there's not string 'APP' in the file. The context of line 1692 (1690-1694) is

thf(ax44,axiom,((subclass_THFTYPE_IiioI @ lAquaticMammal_THFTYPE_i @ lMammal_THFTYPE_i))).

thf(ax45,axiom,((! [PHRASE: $i]: ((instance_THFTYPE_IiioI @ PHRASE @ lPhrase_THFTYPE_i) => (? [PART1: $i,PART2: $i]: ((part_THFTYPE_IiioI @ PART1 @ PHRASE) & (part_THFTYPE_IiioI @ PART2 @ PHRASE) & (instance_THFTYPE_IiioI @ PART1 @ lWord_THFTYPE_i) & (instance_THFTYPE_IiioI @ PART2 @ lWord_THFTYPE_i) & (~ @ (PART1 = PART2)))))))).

%%% notTranslated: (documentation Motion EnglishLanguage "Any &%Process of movement.") SUMO.thf.zip

I'm enclosing the full file and would be grateful for your help.

cbenzmueller commented 2 years ago

Hi Adam,

when you remove the "@" before "(PART1 = PART2)" it works; see below.

Best, C.

thf(ax44,axiom,((subclass_THFTYPE_IiioI @ lAquaticMammal_THFTYPE_i @ lMammal_THFTYPE_i))).

thf(ax45,axiom,((! [PHRASE: $i]: ((instance_THFTYPE_IiioI @ PHRASE @ lPhrase_THFTYPE_i) => (? [PART1: $i,PART2: $i]: ((part_THFTYPE_IiioI @ PART1 @ PHRASE) & (part_THFTYPE_IiioI @ PART2 @ PHRASE) & (instance_THFTYPE_IiioI @ PART1 @ lWord_THFTYPE_i) & (instance_THFTYPE_IiioI @ PART2 @ lWord_THFTYPE_i) & (~ (PART1 = PART2)))))))).

On Mon, 30 May 2022 at 01:43, Adam Pease @.***> wrote:

I tried running Leo-III on the latest SUMO, using output from Sigma's THF translator (written by Christoph). I'm getting

@.***:~/workspace/Leo-III/Leo-III-1.6$ bin/leo3 /home/apease/.sigmakee/KBs/SUMO.thf -t 60 -p % [INFO] Parsing problem /home/apease/.sigmakee/KBs/SUMO.thf ... % OUT OF CHEESE ERROR +++ MELON MELON MELON +++ REDO FROM START % SZS status SyntaxError for /home/apease/.sigmakee/KBs/SUMO.thf : Parse error in file '/home /apease/.sigmakee/KBs/SUMO.thf' in line 1692:309. Unrecognized thf formula input 'APP'

But there's not string 'APP' in the file. The context of line 1692 (1690-1694) is

thf(ax44,axiom,((subclass_THFTYPE_IiioI @ lAquaticMammal_THFTYPE_i @ lMammal_THFTYPE_i))).

thf(ax45,axiom,((! [PHRASE: $i]: ((instance_THFTYPE_IiioI @ PHRASE @ lPhrase_THFTYPE_i) => (? [PART1: $i,PART2: $i]: ((part_THFTYPE_IiioI @ PART1 @ PHRASE) & (part_THFTYPE_IiioI @ PART2 @ PHRASE) & (instance_THFTYPE_IiioI @ PART1 @ lWord_THFTYPE_i) & (instance_THFTYPE_IiioI @ PART2 @ lWord_THFTYPE_i) & (~ @ (PART1 = PART2)))))))).

%%% notTranslated: (documentation Motion EnglishLanguage "Any &%Process of movement.") SUMO.thf.zip https://github.com/leoprover/Leo-III/files/8794515/SUMO.thf.zip

I'm enclosing the full file and would be grateful for your help.

— Reply to this email directly, view it on GitHub https://github.com/leoprover/Leo-III/issues/71, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABGB4RL753232BXZVZDIXZDVMP6LTANCNFSM5XI36DQQ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

lex-lex commented 2 years ago

Alternatively, usage of "connectives as terms", as in negation applied to X, needs to be but in parentheses in THF (this was changed a few years ago, when I recall correctly), e.g., ...

(~) @ (PART1 = PART2)

... is valid THF and can be parsed by Leo-III.

As full formula:

thf(ax45,axiom,((! [PHRASE: $i]: ((instance_THFTYPE_IiioI @ PHRASE @ lPhrase_THFTYPE_i) => (? [PART1: $i,PART2: $i]: ((part_THFTYPE_IiioI @ PART1 @ PHRASE) & (part_THFTYPE_IiioI @ PART2 @ PHRASE) & (instance_THFTYPE_IiioI @ PART1 @ lWord_THFTYPE_i) & (instance_THFTYPE_IiioI @ PART2 @ lWord_THFTYPE_i) & ((~) @ (PART1 = PART2)))))))).

Hope this helps!

Best, Alex

apease commented 2 years ago

Many thanks! I'll see if I can update the translation code