2019-09-04 12:3:43 (GMT)
2019-09-04 12:9:53 (GMT)
If you have a formula F[x] which becomes 10 clauses C1[x]…, C10[x]
2019-09-04 12:10:10 (GMT)
instead, let p[x] be a fresh literal (maximal in the order?)
2019-09-04 12:10:42 (GMT)
Then you produce ¬p[x] ∨ C1[x], … , ¬p[x] ∨ C10[x]
2019-09-04 12:11:3 (GMT)
and then for enumerating each clause independently, you enumerate p[a], p[b], … instead and let CLC do the rest.
edit: this is actually a form of formula renaming, except you wouldn't normally do it, and it marks the predicate p as available only for HO instantiation and for unordered unit resolution.
2019-09-04 12:23:51 (GMT)
I like the idea @Sophie, if the heuristic could look at the whole active set at each step to pick one clause (the "best" clause to perform costly inferences on).
2019-09-04 12:33:11 (GMT)
Plans for the release: cleanup on new branch obtained from merge(lzip+master), cleanup options (for scheduling), release 1.6
2019-09-04 12:33:19 (GMT)
Plans for after the release:
- better CNF
2019-09-04 12:53:39 (GMT)
2019-09-04 13:3:0 (GMT)
Avatar light improvements:
- maybe use minisat/batsat as a solver instead of msat (challenge: proof checking?)
- refine split inference so that C ∨ p1 ∨ p2 where p1,p2 are actual atoms (not terms) becomes C <- ¬p1, ¬p2 (pure boolean literals live purely in the SAT solver). ⇒ means we could parse dimacs problems and solve them in pure SAT.
2019-09-04 13:3:43 (GMT)
= @ lhs @ rhs
2019-09-04 13:23:55 (GMT)
@Sophie @Alexander Bentkamp @Petar Vukmirovic so, next meeting in roughly one month, same setup/hour?
2019-09-04 16:0:36 (GMT)
Validation of grammar, there are some parser generators it seems:
- http://www.nongnu.org/bnf/
- https://bnfc.digitalgrammars.com/
2019-09-04 19:26:13 (GMT)
Unfortunately, the notation is different from the one in the TPTP:
nongnu.org:
factor = IO | name | '[' expression ']' | '&{' expression '&}';
bnfc:
EAdd. Exp ::= Exp "+" Exp1 ;
In the TPTP it looks like this:
<fof_annotated> ::= fof(<name>,<formula_role>,<fof_formula> <annotations>).
2019-09-05 9:24:57 (GMT)
roughly one month is fine with me but I would rather avoid Tuesdays and Wednesdays afternoon if possible. What date/time do you have in mind?
2019-09-05 14:34:36 (GMT)
Nothing in particular, really, same hours (or later) would be good; date is reasonably flexible.
2019-09-06 8:7:20 (GMT)
Ok, I am also flexible, but just to make a concrete proposal: How about October 7? Maybe 3pm Amsterdam time? Then Simon can sleep a little longer.
2019-09-06 8:7:35 (GMT)
That's a Monday.
2019-09-16 12:0:10 (GMT)
Fine with me. I am blocking the date.
2019-10-01 7:15:5 (GMT)
(deleted)