2020-07-04 15:52:16 (GMT)
@Stephan Schulz curious to hear about a java implementation, it should be significantly faster :slight_smile:
2020-07-04 15:54:57 (GMT)
Although it was interesting to note that indexing had less of an impact than subsumption... e.g. being clever was better than being faster.
2020-07-04 16:1:16 (GMT)
Simon Cruanes said:
Stephan Schulz curious to hear about a java implementation, it should be significantly faster :slight_smile:
The idea was that I build a prover in Python, and Adam re-builds it in Java to show that he got it. But real life time constraints intervened (and having Python lists/s-expressions for terms give you a huge initial boost).
2020-07-04 16:3:57 (GMT)
Giles said:
Although it was interesting to note that indexing had less of an impact than subsumption... e.g. being clever was better than being faster.
Yes. If you don't have decent search methods (both heuristics and calculus-wise), speed is useless. You will just run nowhere faster....
2020-07-04 17:16:4 (GMT)
But if you do have decent methods, speed makes a difference :)
2020-07-04 18:24:52 (GMT)
It was a very interesting talk Stephan :slight_smile:
As one of those silly students that had to hack E I have to make a comment about one sentence you made.
You said something along the lines Students found PyRes easier to read than the papers.
This made me think that it is actually documentation for our provers that is bad, not the sheer complexity.
2020-07-04 18:26:28 (GMT)
Out of curiosity, for superposition solvers, is it like for SAT that there are implementation tricks that are very important but written in no paper?
2020-07-04 18:27:50 (GMT)
(one example is https://www.msoos.org/2016/03/memory-layout-of-clauses-in-minisat/, so there is some documentation here, but there is rarely a comment to that blog post)
2020-07-04 18:28:27 (GMT)
Namely, in your PyRes you do have much of the complexity of E (and in my experience, for a single purpose hack, 95% of E code-base can be ignored).
What I think happened, is that Python is easier to understand and in some sense self-documenting and made students understand basic concepts easier.
Do you think it is then maybe a worthwhile project to make better E documentation? Maybe written by a software engineering student (they LOVE to write those documents).
Did you actually have any projects done in PyRes and how did students respond to it?
2020-07-04 18:39:57 (GMT)
No, I don't think the complexity of PyRes is remotely that of E. Just look at main() in eprover.c and __main__() in pyres-fof.py. And that is where people start reading. For E, I think we need to refactor at least a) Indexing and b) main() to make it easier to hack and maintain. I have ideas for both, but limited time. I also think ProcessClause() needs an overhaul.
2020-07-04 18:43:5 (GMT)
Mathias Fleury said:
Out of curiosity, for superposition solvers, is it like for SAT that there are implementation tricks that are very important but written in no paper?
Probably in heaps. But it's hard for me to think about things where we have definite knowledge. But one anecdote from 1996 is me and Bill McCune arguing for 3 hours during the conference trip about some detail of the given clause loop. We finally figured out that what everyone thought was the given-clause algorithm actually had two quite different versions (what we now call the Otter loop and the Discount loop).
2020-07-04 18:52:33 (GMT)
Did I understand correctly that you use PyRes to prepare students to work with E, and/or are there also students that do a project with PyRes?
2020-07-04 19:8:56 (GMT)
I've started using students to introduce them to E last fall, and it worked great. I get the next round in in November...so Corona wills..
2020-07-04 19:42:56 (GMT)
ok thanks for the answer
2020-07-04 21:14:52 (GMT)
Mathias Fleury said:
Out of curiosity, for superposition solvers, is it like for SAT that there are implementation tricks that are very important but written in no paper?
@Stephan Schulz has great slides from a summer school (I think) about the implementation of E. Among the critical tricks that may or not be spelled in details in papers, I think term sharing is a big one; the rewriting steps cached in terms using a pointer and timestamp.
I recall an old paper about Gandalf (🧙) and the best way to implement subsumption checks; also papers on how to implement KBO/LPO efficiently.
A survey paper on implementation would certainly be nice!
2020-07-04 21:32:59 (GMT)
Well, one of the things I wanted to explore with E was shared terms (and shared rewriting). Shared terms work great (shared destructive rewriting not so much), and once you have share terms, you can do a lot (e.g. cache rewrite steps and normal form information). The first (nearly trivial) trick I learned from DISCOUNT was to store a weight (2 for function symbols, 1 for variables) in each term. A heavier term can never match a lighter one, one be a subterm of a lighter one.
2020-07-04 21:40:9 (GMT)
Simon may be talking about http://wwwlehre.dhbw-stuttgart.de/~sschulz/PAPERS/Schulz-VTSA-2009.pdf
2020-07-05 18:45:23 (GMT)
Maybe PyRes could be a good candidate for writing a FOL equivalent of the MiniSAT paper.
2020-07-05 19:16:53 (GMT)
I fully agree. I used to complain to Daniel Wand that there's no MiniSUP. It's a good think that Stephan's mailbox has 0 unread emails and that he'll soon be done with teaching for a while. ;)
2020-07-05 19:17:24 (GMT)
Judging from the (very low) number of CADE/IJCAR papers these days about superposition, it wouldn't hurt to recruit a new generation.
2020-07-05 20:58:35 (GMT)
Isn't Metis kind of minisup?
2020-07-06 5:44:45 (GMT)
It's 20 000 lines long... I don't know why it's that big. Maybe it's just the coding style.
2020-07-06 5:45:1 (GMT)
(And for some strange reason, it's only doing ordered paramodulation.)
2020-07-06 9:11:0 (GMT)
Note that PyRes is resolution only and that Stephan's last remark was that supporting full superposition would increase the footprint of PyRes significantly (hence no future work)
2020-07-06 9:29:50 (GMT)
Of course. I can see that. I also learned superposition by first learning resolution (and its completeness proof) and it makes total sense.
2020-07-06 14:53:59 (GMT)
Well, take a look at the code. I've had some ideas for teaching projects - add miniscoping, add definitions, add set-of-support, add better indexing, add (partial) ordered resolution (e.g. order by predicate only),.... It might be a good idea for me to design a course around it - our electives are in the 4th and 5th semester - the fourth ends in mid May, so I could coax students to build their individual improvements, have a local competition, and then merge everything into a super-pyres for CASC. The courses have (nominally) 24 hours, and it might be too late for next spring (there is an administrative procedure). I'm a bit reluctant, because at the moment I don't teach during the 4th semester, and that is a good thing ;-).
2020-07-06 14:57:9 (GMT)
I'd like to take a look at the code, but I think I'll take a lazy approach here... Already too many fires to put out, unfortunately. :S I'd also like to read your 2009 "Implementing a Theorem Prover" document. Maybe that will come first.
2020-07-06 15:2:26 (GMT)
@Stephan Schulz I currently teach a 'Symbolic AI ' course where I start with forward/backward chaining (we use AI: A Modern Approach by Russel and Norvig ). I give them some python code for forward/backward chaining and ask them to edit it to help understanding. I chose to write my one instead of using https://github.com/aimacode/aima-python as that code is a bit complicated.
I then give them Vampire and the tasks are more about inspecting the output. I'm thinking I could add PyRes to this picture to get them to understand the basics (I teach given clause algorithm, clause selection, literal selection). I'll probably have look in Jan/Feb when I do my course revision :)
2020-07-06 20:29:30 (GMT)
@Giles You are very welcome. Check e.g. unification or indeed the ProofState, which implements the given-clause algorithm.