Student Work

 

A Tactic For Setoid Congruence Public

Downloadable Content

open in viewer

The congruence tactic built into the Coq proof management system allows for solving entailment of closed equalities with uninterpreted function symbols. In this project we build a congruence tactic that works with multiple relations. My theoretical contribution is to describe a translation from entailments in a generalized form of congruence into the traditional form that existing algorithms can solve. The tactic makes use of this transformation, as well as an implementation of congruence closure, to solve Coq goals involving multiple relations.

  • 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-050521-204339
  • 22476
Advisor
Year
  • 2021
Date created
  • 2021-05-05
Resource type
Major
Rights statement
License

Relationships

In Collection:

Items

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