Intuitionistic completeness of first-order logic (Q392280): Difference between revisions

@@ Property / describes a project that uses @@
+Twelf
@@ Property / describes a project that uses: Twelf / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nuprl
@@ Property / describes a project that uses: Nuprl / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W1999807931
@@ Property / OpenAlex ID: W1999807931 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q55967618
@@ Property / Wikidata QID: Q55967618 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.1614
@@ Property / arXiv ID: 1110.1614 / rank @@
+Normal rank
@@ Property / cites work @@
+Innovations in computational type theory using Nuprl
+Normal rank
@@ Property / cites work @@
+Q4499151
@@ Property / cites work: Q4499151 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5316409
@@ Property / cites work: Q5316409 / rank @@
+Normal rank
@@ Property / cites work @@
+Do-it-yourself type theory
@@ Property / cites work: Do-it-yourself type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q4524766
@@ Property / cites work: Q4524766 / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Q5792923
@@ Property / cites work: Q5792923 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3235350
@@ Property / cites work: Q3235350 / rank @@
+Normal rank
@@ Property / cites work @@
+The foundations of mathematics. A study in the philosophy of science
+Normal rank
@@ Property / cites work @@
+Q4981439
@@ Property / cites work: Q4981439 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5573965
@@ Property / cites work: Q5573965 / rank @@
+Normal rank
@@ Property / cites work @@
+A Brief Overview of Agda – A Functional Language with Dependent Types
+Normal rank
@@ Property / cites work @@
+Q5670174
@@ Property / cites work: Q5670174 / rank @@
+Normal rank
@@ Property / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+Q5753923
@@ Property / cites work: Q5753923 / rank @@
+Normal rank
@@ Property / cites work @@
+An application of constructive completeness
@@ Property / cites work: An application of constructive completeness / rank @@
+Normal rank
@@ Property / cites work @@
+Combinatory logic. With two sections by William Craig.
+Normal rank
@@ Property / cites work @@
+Q4133603
@@ Property / cites work: Q4133603 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5582318
@@ Property / cites work: Q5582318 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3994895
@@ Property / cites work: Q3994895 / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Q5339292
@@ Property / cites work: Q5339292 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4288818
@@ Property / cites work: Q4288818 / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Q4757531
@@ Property / cites work: Q4757531 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5724783
@@ Property / cites work: Q5724783 / rank @@
+Normal rank
@@ Property / cites work @@
+Intuitionism. An introduction
@@ Property / cites work: Intuitionism. An introduction / rank @@
+Normal rank
@@ Property / cites work @@
+Q4068683
@@ Property / cites work: Q4068683 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3204055
@@ Property / cites work: Q3204055 / rank @@
+Normal rank
@@ Property / cites work @@
+Continuation-passing style models complete for intuitionistic logic
+Normal rank
@@ Property / cites work @@
+On the interpretation of intuitionistic number theory
+Normal rank
@@ Property / cites work @@
+Q5812175
@@ Property / cites work: Q5812175 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5343325
@@ Property / cites work: Q5343325 / rank @@
+Normal rank
@@ Property / cites work @@
+Zur Deutung der intuitionistischen Logik
@@ Property / cites work: Zur Deutung der intuitionistischen Logik / rank @@
+Normal rank
@@ Property / cites work @@
+On weak completeness of intuitionistic predicate logic
+Normal rank
@@ Property / cites work @@
+Q5509675
@@ Property / cites work: Q5509675 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5619069
@@ Property / cites work: Q5619069 / rank @@
+Normal rank
@@ Property / cites work @@
+Syntactic translations and provably recursive functions
+Normal rank
@@ Property / cites work @@
+Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels
+Normal rank
@@ Property / cites work @@
+Q5181669
@@ Property / cites work: Q5181669 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4099613
@@ Property / cites work: Q4099613 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3328540
@@ Property / cites work: Q3328540 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247306
@@ Property / cites work: Q4247306 / rank @@
+Normal rank
@@ Property / cites work @@
+Undecidability and intuitionistic incompleteness
@@ Property / cites work: Undecidability and intuitionistic incompleteness / rank @@
+Normal rank
@@ Property / cites work @@
+Completeness and incompleteness for intuitionistic logic
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2778806
@@ Property / cites work: Q2778806 / rank @@
+Normal rank
@@ Property / cites work @@
+LCF considered as a programming language
@@ Property / cites work: LCF considered as a programming language / rank @@
+Normal rank
@@ Property / cites work @@
+Q5734410
@@ Property / cites work: Q5734410 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4843182
@@ Property / cites work: Q4843182 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4214829
@@ Property / cites work: Q4214829 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5560258
@@ Property / cites work: Q5560258 / rank @@
+Normal rank
@@ Property / cites work @@
+Lectures on the Curry-Howard isomorphism
@@ Property / cites work: Lectures on the Curry-Howard isomorphism / rank @@
+Normal rank
@@ Property / cites work @@
+Q3998865
@@ Property / cites work: Q3998865 / rank @@
+Normal rank
@@ Property / cites work @@
+An intuitionistically plausible interpretation of intuitionistic logic
+Normal rank
@@ Property / cites work @@
+Intensional interpretations of functionals of finite type I
+Normal rank
@@ Property / cites work @@
+Q4003339
@@ Property / cites work: Q4003339 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4215635
@@ Property / cites work: Q4215635 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructivism in mathematics. An introduction. Volume II
+Normal rank
@@ Property / cites work @@
+An intuitiomstic completeness theorem for intuitionistic predicate logic
+Normal rank