scientific article; zbMATH DE number 863013
From MaRDI portal
Publication:4871733
Recommendations
Cited in
(20)- Automating Proofs in Category Theory
- Proof search with set variable instantiation in the calculus of constructions
- On the proof theory of Coquand's calculus of constructions
- scientific article; zbMATH DE number 2185723 (Why is no real title available?)
- scientific article; zbMATH DE number 978243 (Why is no real title available?)
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Automatic Abstraction for Congruences
- From cut-free calculi to automated deduction: the case of bounded contraction
- A mechanized proof system of the third generation calculus in Coq
- scientific article; zbMATH DE number 3894495 (Why is no real title available?)
- M-calculus -- a sequent method for automatic theorem proving
- scientific article; zbMATH DE number 6938205 (Why is no real title available?)
- On connections and higher-order logic
- A Complete Proof Synthesis Method for the Cube of Type Systems
- Autarkic computations in formal proofs
- Developing certified programs in the system Coq the program tactic
- Theory of types and decision procedures
- The calculus of constructions as a framework for proof search with set variable instantiation
- Proof-term synthesis on dependent-type systems via explicit substitutions
- scientific article; zbMATH DE number 4019061 (Why is no real title available?)
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4871733)
