_roadmap.md

Road Map for Checking the Trace Format

Participant:

• Xaviera Steele

Supervision:

• Tomer Libal

Macro steps:

• understanding propositional and first-order logic
• programming in Prolog
• writing a trusted kernel in Prolog for propositional logic
• adding proof guidance to the kernel without harming its soundness
• understanding propositional resolution and being able to read the Trace format
• writing a program (in Python?) which translates a Trace proof into a Prolog file
• writing a Prolog program which can guide the search in the kernel based on the translated input proof
• writing a program (Python/shell) which apply the three programs together
• testing on simple examples
• using BoolForce in order to generate traces of real SAT problems
• what are the limits of the certification tool? How does it compare to the TraceCheck tool?

See the progress page for more information.

Possible outcomes:

• PxTP paper?