Student Work

 

Formal Verification of Boolean Unification Algorithms with Coq Public

Downloadable Content

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.

Creator
Publisher
Identifier
  • E-project-042419-212433
Advisor
Year
  • 2019
Date created
  • 2019-04-24
Resource type
Major
Rights statement
License

Relationships

In Collection:

Items

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