Proof-search in type-theoretic languages: an introduction

Proof-search in type-theoretic languages: an introduction

Source :

• Theoretical Computer Science [ 0304-3975 ] ; 2000.

English descriptors

• Teeft :
  • Academic press, Algebraic, Algorithm, Answer substitution, Atomic positions, Automat, Avron, Axiom, Basic idea, Boolean constraints, Cade, Cade workshop, Calculus, Cambridge university press, Category theory, Cient, Classical logic, Classical search, Classical sequent calculus, Comput, Computational, Computer, Computer science, Conf, Consequence relation, Consequence relations, Constructive program synthesis, Constructive type theory, Deductive systems, Dependent types, Electronic notes, Encoding, Erent, Formula tree, Framework, Function space, Functional programming, Functorial models, Galmiche, Girard, Herbrand, Herbrand models, Herbrand structure, Hereditary harrop formulae, Inductive, Inference rules, Interactive, Interactive theorem provers, Internal logic, Internal structure, Internat, Intuitionistic, Intuitionistic logic, Intuitionistic logics, Intuitionistic propositional logic, Intuitionistic provability, Judgement, July, Kripke, Kripke models, Lambda calculus, Lecture notes, Linear logic, Linear logic programming, Logic, Logic comput, Logic programming, Logic programming language, Logical framework, Logical frameworks, Logical systems, Matrix, Minimal logic, Modal logics, Natural deduction, Natural deduction systems, Normal proofs, Nuprl, Operational semantics, Other logics, Oxford university press, Parigot, Petri nets, Pfenning, Predicate, Predicate logic, Proc, Program synthesis, Programming, Programming language, Proof nets, Proof nets construction, Proof search, Proof system, Proof systems, Proof theory, Proof transformations, Proofsearch, Propositional, Propositional intuitionistic logic, Provability, Provable, Prover, Provers, Pure appl, Representation mechanism, Resolution calculus, Saratoga springs, Satisfaction relation, Search procedure, Search space, Semantics, Sequent, Sequent calculi, Sequent calculus, Sequents, Single publication, Springer, Structural rules, Substructural, Substructural logics, Symbolic logic, Tableau, Theorem provers, Theoret, Theoretical computer science, Typable terms, Type system, Type systems, Type theories, Type theory, Uniform proofs, Wallen.

Abstract

• https://api.istex.fr/ark:/67375/6H6-1F1HBVPL-L/fulltext.pdf

Affiliations:

• France, Royaume-Uni
• Angleterre, Grand Est, Grand Londres, Lorraine (région)
• Londres, Vandœuvre-lès-Nancy
• Université Henri Poincaré, Université de Londres

Links toward previous steps (curation, corpus...)

• to stream Istex, to step Corpus: 001656
• to stream Istex, to step Curation: 001637

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Checkpoint

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001F70 | SxmlIndent | more

Ou

HfdSelect -h $EXPLOR_AREA/Data/Istex/Checkpoint/biblio.hfd -nk 001F70 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Istex
   |étape=   Checkpoint
   |type=    RBID
   |clé=     ISTEX:60F3E329459D751A183454414CCCEB80DC4A947E
   |texte=   Proof-search in type-theoretic languages: an introduction
}}

This area was generated with Dilib version V0.6.33. Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022