back to root

back to Zipperposition

meeting 2020-02-18

• Simon Cruanes

  2020-02-13 19:3:42 (GMT)

  agenda (tell me what's missing so I can add it, or reply):

  • workshop (main topic)
  • progress report from @Petar Vukmirovic about bools, sine, scheduling, etc. ? :)
  • talk about releasing 1.6.1
  • modularity efforts (zip-lite? split HO/arith/induction into sub-libs? open literals?)
  • basic support for $real

• Alexander Bentkamp

  2020-02-13 19:53:42 (GMT)

  • merge of lambda-free and lambda branches (work in progress)

• Simon Cruanes

  2020-02-18 15:29:10 (GMT)

  Summary for the tutorial:

  • first part: simple prover to show off logtk

    • poke holes in resolution1.ml, make it a hand-on (with a VM and list of problems)

      • no index at first?
      • no factoring?
      • Clause.is_trivial

    • find not too hard benchs (agatha?).
      Also a test-bed that runs the prover on select problems, and colors green/red.
      This way, easy to measure improvements.

    • add some basic improvements (ordering? selection?)

    • pick some problems so that some are solved by the basic solver,
      but improvements (filling holes) solve more

    • NOTE: remove signature entirely? or keep it for later improvements like orderings?

    • make a VM with everything preinstalled (vagrant?)
      (need virtualbox)

  • second part: implement, say, tuples.

    • start with encoding, which works but has shortcomings (explosive clauses)
    • need holes too (preimplement parsing TFX/THX + typing)
    • have empty theory to deal with tuples (with comments for guidance)
    • discuss calculus rules beforehand!
  • put everything in the matryoshka repo? or zipper repo?
  • proper rehearsal in Amsterdam (May/June?)
  • capture the flag: first one to solve the problem "captures its flag"

• Simon Cruanes

  2020-02-20 1:8:6 (GMT)

  I have a vagrantfile for building a VM on wip-vagrant-vm (you need virtualbox and vagrant to build it):

  • cd utils/
  • vagrant up --provision
  • vagrant ssh (or use the virtualbox interface to log in graphically).

  It should contain zipperposition and a few editors.