Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

12

CORR
2010
Springer

favoriteEmaildiscussreport

158views Education» more CORR 2010»

A Minimal Propositional Type Theory

13 years 4 months ago

A Minimal Propositional Type Theory

Download www.ps.uni-saarland.de

Propositional type theory, first studied by Henkin, is the restriction of simple type theory to a single base type that is interpreted as the set of the two truth values. We show that two constants (falsity and implication) suffice for denotational and deductive completeness. Denotational completeness means that every value of the full set-theoretic type hierarchy can be described by a closed term. Deductive completeness is shown for a sequent-based proof system that extends a propositional natural deduction system with lambda conversion and Boolean replacement.

Mark Kaminski, Gert Smolka

Real-time Traffic

CORR 2010 | Deductive Completeness | Education | Propositional Type Theory | Type Theory |

claim paper

Related Content

» Quotients over Minimal Type Theory

» Pattern minimization problems over recursive data types

» Extensional Equality in Intensional Type Theory

» Markovs Principle for Propositional Type Theory

» A Modular Typechecking algorithm for Type Theory with Singleton Types and Proof Irrelevanc...

» On Computing Backbones of Propositional Theories

» PASSAGE Syntactic Representation a Minimal Common Ground for Evaluation

» On the Complexity of Theory Curbing

» Minimal Logic Programs

Post Info
More Details (n/a)

Added	09 Dec 2010
Updated	09 Dec 2010
Type	Journal
Year	2010
Where	CORR
Authors	Mark Kaminski, Gert Smolka

Comments (0)