Congruence Closure in Intensional Type Theory

DOI10.1007/978-3-319-40229-1_8zbMath1475.68452arXiv1701.04391OpenAlexW2506025915MaRDI QIDQ2817913

Leonardo de Moura, Daniel Selsam

Publication date: 5 September 2016

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1701.04391

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)

Related Items (1)

Hammer for Coq: automation for dependent type theory

Uses Software

• Coq
• z3
• SIMPLIFY
• Matita
• CVC4
• Epigram
• Agda
• Irdis
• Lean
• Idris
• Heq

Cites Work

• Abstract congruence closure
• Programming up to Congruence
• A Brief Overview of Agda – A Functional Language with Dependent Types
• The Lean Theorem Prover (System Description)
• Simplify: a theorem prover for program checking
• Fast Decision Procedures Based on Congruence Closure
• Shostak's congruence closure as completion
• The Matita Interactive Theorem Prover
• A Machine-Checked Proof of the Odd Order Theorem
• Advanced Functional Programming
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Term Rewriting and Applications
• Types for Proofs and Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Congruence Closure in Intensional Type Theory