The calculus of constructions as a framework for proof search with set variable instantiation
From MaRDI portal
Publication:1575927
DOI10.1016/S0304-3975(99)00175-9zbMath0952.03005OpenAlexW1972358050MaRDI QIDQ1575927
Publication date: 23 August 2000
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0304-3975(99)00175-9
Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Logic programming (68N17)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The calculus of constructions
- Implementing tactics and tacticals in a higher-order logic programming language
- SET-VAR
- \({\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
- Proof search with set variable instantiation in the Calculus of Constructions
- Introduction to generalized type systems