cbenzmueller
commented
4 years ago Dear Dan,
yes, you should definitely obey the TPTP language conventions, otherwise symbols might get wrongly interpreted. The implementation of some back and forth translation table can eventually be useful in your case.
Best, C.
Christoph Benzmüller, Dr. habil., Professor Freie Universität Berlin, Dep. of Mathematics and Computer Science, 14195 Berlin Further Affiliations: Université du Luxembourg, FSTC, Avenue de l'Université, L-4365 Esch-sur-Alzette, Luxembourg Saarland University, Dep. of Computer Science, Saarbrücken http://christoph-benzmueller.de c.benzmueller@gmail.com | christoph.benzmueller@uni.lu | c.benzmueller@fu-berlin.de
On Tue, Mar 10, 2020 at 10:06 AM Dan Welch notifications@github.com wrote:
Hi all, apologies if there was a better place to post this question. I've been messing around with the tool for about a month now (specifically the thf1 language) and am quite impressed with it and its higher order reasoning capabilities. I hope to use it eventually as a backend solver for a program verifier (written in Java) that I've been working on that produces verification conditions (VCs) as sequents involving higher order terms.
Note that I'd prefer (if feasible) to convert the terms and types from my source language to LEO III programmatically (as opposed to simply generating a TPTP 'script' and feeding it in). Question:
So after cloning and investigating LEO III's codebase, do Commons.THFAnnotated classes -- if constructed programmatically -- still require the capitalization and naming conventions that the TPTP requires? Just asking as source terms and definitions in my tool include some unicode chars as well as capitals, naturally.. Any idea if this will mess up internal algorithms if I forgo LEO's parser -- and hence the TPTP naming conventions enforced as part of the standard?
Just figured I'd ask and save myself the time before going ahead and mangling names read in from my tool's sourcefiles (though it wouldn't be the end of the world if I had to do so; just harder to read stuff in debuggers, printouts, etc :-)
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/leoprover/Leo-III/issues/65?email_source=notifications&email_token=ABGB4RI7SEOET4CZGKYI6KTRGX7K5A5CNFSM4LE2FTLKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IT2FSAA, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABGB4ROBAFFBC2SYTRGKD43RGX7K5ANCNFSM4LE2FTLA .
dtwelch
Hi all, apologies if there was a better place to post this question. I've been messing around with the tool for about a month now (specifically the thf1 language) and am quite impressed with it and its higher order reasoning capabilities. I hope to use it eventually as a backend solver for a program verifier (written in Java) that I've been working on that produces verification conditions (VCs) as sequents involving higher order terms.
Note that I'd prefer (if feasible) to convert the terms and types from my source language to LEO III programmatically (as opposed to simply generating a TPTP 'script' and feeding it in).
Question:
So after cloning and investigating LEO III's codebase, do
Commons.THFAnnotatedclasses -- if constructed programmatically -- still require the capitalization and naming conventions that the TPTP requires? Just asking as source terms and definitions in my tool include some unicode chars as well as capitals, naturally.. Any idea if this will mess up internal algorithms if I forgo LEO's parser -- and hence the TPTP naming conventions enforced as part of the standard?Just figured I'd ask and save myself the time before going ahead and mangling names read in from my tool's sourcefiles (though it wouldn't be the end of the world if I had to do so; just harder to read stuff in debuggers, printouts, etc :-)