TPTP

[dr.mt...@gmail.com]

Or Thousands of Problems for Theorem Provers is a cool site for those interested in testing ATPs.  One problem is that the syntax of TPTP is not that of THORN and transcribing by hand is too tedious.  It's a nice study for a Shen programmer to be able to type securely compile this enormous library into THORN notation and use it to test THORN.   

It's a good final year UG project.

M.

[dr.mt...@gmail.com]

One first-order theory is over 4 x 10^5 lines long (400, 991 to be exact), take a gander.  

I'm going to see if this can be parsed into THORN notation using Shen YACC.  I've never

tried to parse a file of this size before and compiling it into THORN should be a challenge.

M.

[dr.mt...@gmail.com]

Well, under Shen/Scheme, parsing this file into THORN first order axioms using Shen-YACC took 10.8 seconds.
Writing the resulting THORN axioms to file took 13.6 seconds.  Compiling this knowledge base into executable

Shen via the THORN compiler takes a lot longer.  

M.

[Bruno Deferrari]

On Fri, Jun 30, 2023 at 6:54 PM dr.mt...@gmail.com <dr.mt...@gmail.com> wrote:

Well, under Shen/Scheme, parsing this file into THORN first order axioms using Shen-YACC took 10.8 seconds.
Writing the resulting THORN axioms to file took 13.6 seconds.  Compiling this knowledge base into executable

Shen via the THORN compiler takes a lot longer.  

Regarding this part "Writing the resulting THORN axioms to file took 13.6 seconds."

How much data is it? and which functions are you using for writing the data? Shen/Scheme already tries to use fast native options when possible for the standard Shen I/O functions, but for your specific case there may be specific native calls that can speed it up.

 

M.

On Tuesday, 27 June 2023 at 13:42:35 UTC+1 dr.mt...@gmail.com wrote:

One first-order theory is over 4 x 10^5 lines long (400, 991 to be exact), take a gander.  

I'm going to see if this can be parsed into THORN notation using Shen YACC.  I've never

tried to parse a file of this size before and compiling it into THORN should be a challenge.

M.

On Thursday, 8 June 2023 at 22:25:02 UTC+1 dr.mt...@gmail.com wrote:

Or Thousands of Problems for Theorem Provers is a cool site for those interested in testing ATPs.  One problem is that the syntax of TPTP is not that of THORN and transcribing by hand is too tedious.  It's a nice study for a Shen programmer to be able to type securely compile this enormous library into THORN notation and use it to test THORN.   

It's a good final year UG project.

M.

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/b8f47ade-aa1c-4ca9-9063-dca6d49ddd76n%40googlegroups.com.

--

BD

[dr.mt...@gmail.com]

On Friday, 30 June 2023 at 23:47:45 UTC+1 Bruno Deferrari wrote:

On Fri, Jun 30, 2023 at 6:54 PM dr.mt...@gmail.com <dr.mt...@gmail.com> wrote:

Well, under Shen/Scheme, parsing this file into THORN first order axioms using Shen-YACC took 10.8 seconds.
Writing the resulting THORN axioms to file took 13.6 seconds.  Compiling this knowledge base into executable

Shen via the THORN compiler takes a lot longer.  

Regarding this part "Writing the resulting THORN axioms to file took 13.6 seconds."

How much data is it? and which functions are you using for writing the data? Shen/Scheme already tries to use fast native options when possible for the standard Shen I/O functions, but for your specific case there may be specific native calls that can speed it up.

 25.663 Mb.

(define bench
  File -> (let Props (time (compile (fn <axioms>) (read-file-as-bytelist File)))
                    Out   (open "props.shen" out)
                    Write (mapc (/. X (pr (make-string "~S~%~%" X) Out)) Props)
                    (close Out)))

M.

[dr.mt...@gmail.com]

The real problem is not writing the THORN axioms to disk.  It's reading them in.  There is one 

expression which extends to column 51,209 and is nested to a depth of over 600 parentheses.

It seems the Shen reader chokes on this.

M.

[dr.mt...@gmail.com]

I take it back - it reads it and the other 10,000 lines in 1.23 sec.  

[dr.mt...@gmail.com]

I think the real challenge is getting the THORN compiler to digest this huge mass.  It may be that there is a non-linear

relation between the size of some of these axioms and the time taken to compile them.    I'm testing on a set of 100

lines, 1000 lines, 10,000 lines.    The first two compile fine.

(0-) (load "100.txt")
compiled

run time: 0.046875 secs
loaded

(1-) (load "1000.txt")
compiled

run time: 0.46875 secs
loaded

You see a linear relation here but the 10000 file kills it because, I suspect, it contains some of these humungous axioms

referred to earlier.

M.

[dr.mt...@gmail.com]

In fact there is another whale which stretches out to column 112,687 and has over 1000 nested parens.

M.

[dr.mt...@gmail.com]

Beaten by another which measures a quarter of a million characters in length, probably 2000+ parens.

But the grandaddy Methuselah is a first-order formula that stretches out over half a million characters

(545, 129) and I haven't counted the parens.  And this is only one line in 10,000 lines.

M.