Student Work

Formal Verification of Boolean Unification Algorithms with Coq

公开

可下载的内容

open in viewer

We report on a verified implementation of two (well-known) algorithms for unification modulo the theory of Boolean rings: Lowenheim's method and the method of Successive Variable Elimination. The implementations and proofs of correctness were done in the Coq proof assistant; we view this contribution as an early step in a larger project of developing a suite of verified implementations of equational unification algorithms.

  • This report represents the work of one or more WPI undergraduate students submitted to the faculty as evidence of completion of a degree requirement. WPI routinely publishes these reports on its website without editorial or peer review.
Creator
Publisher
Identifier
  • E-project-042419-212433
Advisor
Year
  • 2019
Date created
  • 2019-04-24
Resource type
Major
Rights statement

关系

属于 Collection:

项目

单件

Permanent link to this page: https://digital.wpi.edu/show/wh246v71v