scientific article; zbMATH DE number 863013
From MaRDI portal
Publication:4871733
zbMATH Open0849.68111MaRDI QIDQ4871733FDOQ4871733
Authors: Gilles Dowek 
Publication date: 2 April 1996
Title of this publication is not available (Why is that?)
Recommendations
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)
Cited In (20)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- \(M\)-calculus -- a sequent method for automatic theorem proving
- Title not available (Why is that?)
- 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
- Proof-term synthesis on dependent-type systems via explicit substitutions
- The calculus of constructions as a framework for proof search with set variable instantiation
- Title not available (Why is that?)
- 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
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)
