search

leoprover / Leo-III

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
http://inf.fu-berlin.de/~lex/leo3
BSD 3-Clause "New" or "Revised" License
41 stars 10 forks source link

$TPTP not recognised #53

Closed andreas-roehler closed 6 years ago

andreas-roehler commented 6 years ago

According to USAGE.md Leo-III should automatically resolve TPTP axioms. In my .bashrc resides export TPTP="$HOME/PATH-TO/TPTP-v7.0.0"

However: java -jar leo3.jar SET014^4.p % [INFO] No timeout was given, using default timeout -t 60 % OUT OF CHEESE ERROR +++ MELON MELON MELON +++ REDO FROM START % SZS status InputError for SET014^4.p : The file /home/speck/arbeit/logik/leo/ar-Leo-III/bin/SET014^4.p does not exist or cannot be read.

While with java -jar leo3.jar FULL-PATH-TO-SET014^4.p it works

Cheers, Andreas

lex-lex commented 6 years ago

TPTP problems are not TPTP axioms. You need to give Leo-III the full path to your input problem. If, however, the input problem contains an TPTP import (import('Axioms/...')), this import will be resolved automatically if $TPTP is set accordingly.

The error message indicates that the problem was not found (not that any axiom file was not found).

andreas-roehler commented 6 years ago

Hmm, for me that distinction isn't visible from USAGE.md It first mentions "axiom", than calling the example "problem":

export TPTP=/path/to/TPTP

If this environment variable is set, Leo-III will automatically resolve TPTP axioms. Example

Let's solve the TPTP problem SET014^4.p (see here) with a timeout of 60 seconds and proof output:

./leo3 SET014^4.p -t 60 -p

lex-lex commented 6 years ago

Well, this example assumes that SET014^4.p is located in your current working directory. If you think this is ambigious, feel free to amend the description.

andreas-roehler commented 6 years ago

On 16.02.2018 00:32, Alexander Steen wrote:

Well, this example assumes that SET014^4.p is located in your current working directory. If you think this is ambigious, feel free to amend to the description.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/leoprover/Leo-III/issues/53#issuecomment-366097776, or mute the thread https://github.com/notifications/unsubscribe-auth/ABHmk_7BQtKlI8zIXNuwrjKValcf5IXbks5tVL6HgaJpZM4SETUc.

IMHO fixing this would mean to provide a suitable example. May look for that.

lex-lex commented 6 years ago

So, since there is nothing to fix regarding the use of $TPTP within Leo-III (at least that I'm aware of), I'm closing this issue. I've updated the example to be more precise in b5aa53734dc93755a8fcaeda68cbbbf34d79428f. Feel free to open another issue if you think something is not working as intended.