Proof search with set variable instantiation in the Calculus of Constructions

DOI10.1007/3-540-61511-3_120zbMath1412.68221OpenAlexW1514169328MaRDI QIDQ4647555

Amy P. Felty

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_120

Mathematics Subject Classification ID

Related Items (1)

The calculus of constructions as a framework for proof search with set variable instantiation

Uses Software

• Coq
• Isabelle
• ML
• HOL
• Nuprl

Cites Work

• The calculus of constructions
• \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
• Isabelle. A generic theorem prover
• Uniform proofs as a foundation for logic programming
• A framework for defining logics
• A Complete Proof Synthesis Method for the Cube of Type Systems
• A formulation of the simple theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proof search with set variable instantiation in the Calculus of Constructions