/propa

Primary LanguageOCaml

Working through HPLAR

This repository houses my reimplementation of John Harrison's Handbook of Practical Logic and Automated Reasoning in more modern OCaml. At the time of writing, it contains:

Chapters 1 and 2

  • A parameterized parser for the formula datatype using menhir. Menhir takes a parameter directive in an .mly file and produces a functor for a parser, which is pretty cool!
  • Pretty printers for propositional formulae.
  • Printing of truth tables of propositional formulae. For example,
let () = 
let fmla = Parse.string "p \\/ (q <==> r) <==> ( p \\/ q <==> p \\/ r)\n" in
  Propositional.pp_truth_table fmla;

prints the following

------------------------------
q      p      r      | (p∨q <=> r) <=> (p∨q) <=> (p∨r)
------------------------------
true   true   true   | true  
false  true   true   | true  
true   false  true   | true  
true   true   false  | true  
true   false  false  | true  
false  false  true   | true  
false  true   false  | true  
false  false  false  | true