Herbrand - Playground for experimenting with decision procedures in Haskell

References

• A. Zeljić: "CS 357 Advanced Topics in Formal Methods".
• G. Nelson and D. C. Oppen: "Fast Decision Procedures Based on Congruence Closure".
• P. J. Downey, R. Sethi, and R. E. Tarjan: "Variations on the Common Subexpression Problem".
• D. C. Oppen: "Complexity, Convexity and Combinations of Theories"
• M. Willsey, C.Nandi, Y. R. Wang, O. Flatt, Z. Tatlock, and P. Panchekha: "egg: Fast and Extensible Equality Saturation". POPL '21.
• R. Mesquita: "hegg: Fast equality saturation in Haskell".
• H. Nabeshima and T. Soh: "高速 SAT ソルバーの原理 (Principles of Modern SAT Solvers)".
• K. Iwanuma and H. Nabeshima: SMT: 個別理論を取り扱うSAT技術 (SMT: Satisfiability Modulo Theories).
• H. H. Hoos and T. Stützle: "SATLib".
• E. Torlak: "A Modern SAT Solver". In the course material of "CSE 507: Computer-Aided Reasoning for Software".
• J. H. Liang, V. Ganesh, E. Zulkoski, A. Zaman, and K. Czarnecki: "Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers".
• H. Wu: "Randomization and Restart Strategies". Master's Thesis. 2006