# Congruence Closure in Intensional Type Theory

## TL;DR

This paper introduces a novel, efficient congruence closure algorithm capable of handling the full expressive power of intensional type theory, including dependent types, which are essential for many theorem proving applications.

## Contribution

It presents the first congruence closure procedure that supports all functions in ITT with dependencies, relying only on the uniqueness of identity proofs axiom.

## Key findings

- Successfully solves verification problems with dependent types
- Supports all functions in ITT regardless of dependencies
- Efficient and proof-producing algorithm

## Abstract

Congruence closure procedures are used extensively in automated reasoning and are a core component of most satisfiability modulo theories solvers. However, no known congruence closure algorithms can support any of the expressive logics based on intensional type theory (ITT), which form the basis of many interactive theorem provers. The main source of expressiveness in these logics is dependent types, and yet existing congruence closure procedures found in interactive theorem provers based on ITT do not handle dependent types at all and only work on the simply-typed subsets of the logics. Here we present an efficient and proof-producing congruence closure procedure that applies to every function in ITT no matter how many dependencies exist among its arguments, and that only relies on the commonly assumed uniqueness of identity proofs axiom. We demonstrate its usefulness by solving interesting verification problems involving functions with dependent types.