679 B
679 B
up, tags, aliases
up | tags | aliases |
---|---|---|
[!proposition]+ On définit une fonction
p
qui à un symbole associe un poids :p(0) = p(1) = p(v) = -1
pour toutv \in V
p(\neg) = 0
p(\wedge) = p(\vee) = p(\implies) = p(\iff) = 1
p(\emptyset) = 0
Puis par réccurence, avecm = [a_1, \dots ,a_{n}]
aveca_{i} \in V \cup L
p(m) = p(a_1) + \cdots + p(a_{n})
On a alors le théorème suivant : Un mot
f
est une formule (bien formée) si et seulement si on a :
p(f) = -1
- pour tout préfixe
f'
def
,f' \neq f
on ap(f') \geq 0
[!corollaire] Un préfixe
f'
d'une formulef
(tel quef' \neq f
) n'est pas uen formule. ^thm