[LOGI] Logique du premier ordre (1)

Modes de definition

C’est quoi definir ?

Mot = mot1 mot2 mot3 … motn

Definition linguistique (ou definition de type dictionnaire)

Mode de definition inductive

Un type est defini par induction lorsqu’on donne :

Exemple : integer

Condition d’arret = s’arreter : Condition

Mots

Les mots (Induction) sur l’alphabet

On note le type obtenu

Logique Propositionnelle

Par induction on cree un type “formule propositionnelle” ou encore type On a donc :

est construit :

Exemple :

Procedure de verification de constructions de type

On observe que

On peut donc discriminer dans avec

Dans > types et non types

On met en entree des mots de et en sortie on a

Algo

Valuation :

ex : V(

Arite : nombre d’elements qui s’accrochent a un symbole

Process

V

Stop at : (a un moment) ou (lecture du dernier symbole)

Theoreme

En choisissant “Accept”, ssi le process s’arrete en validant les 2 conditions, on obtient une procedure de verification de

Exemple :

V 1 1 1 -1 0 -1 1 -1 -1
1 2 3 2 2 1 2 1 0

donc pas de type