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

• McDonald, Matthew Joseph
• Antonatos, Spyridon
• St. Pierre, Joseph Keenan
• Richardson, Dylan

Publisher

• Worcester Polytechnic Institute

Identifier

• E-project-042419-212433

Advisor

• Dougherty, Daniel J.

Year

• 2019

Date created

• 2019-04-24

Resource type

• Major Qualifying Project

Major

• Computer Science

Rights statement

• In Copyright

License

• All rights reserved