Revenons maintenant sur les paragraphes précédents.
Les propositions de base notées par une lettre (P,Q), sans connecteurs, sont appelées quelquefois 'atomes' ou 'variables propositionnelles'.
A ces propositions de base on ajoute les 'constantes' V et F, qui sont les propositions respectivement toujours vraie, toujours fausse.
Par opposition, les propositions construites à partir des atomes et des connecteurs logiques ¬ , ∧ , ∨ s'appellent des 'formules'.
Voici quelques exemples:
(P∨Q)∧(¬ R)
¬(P∨(¬ Q))
Le premier problème est de reconnaître les formules 'bien formées'.
Pour être 'bien formée' , une formule doit obéir à des règles.
L'ensemble de ces règles constitue une 'grammaire' définissant les symboles pouvant être reconnus comme des formules.

Ces formules sont également des propositions pouvant être vues comme des expressions où les variables représentent des assertions plutôt que des nombres ou des vecteurs.
Ces expressions peuvent faire l'objet d'une évaluation. La seule différence avec les expressions numériques est que l'ensemble des valeurs possibles se réduit à deux éléments {V,F}.
C'est bien pour cela qu'on parle de 'calcul propositionnel', tout à fait semblable dans son esprit au calcul numérique.
Un ordinateur peut, grâce à un programme spécial, appelé analyseur syntaxique, décider si une expression est correcte et construire l'arbre correspondant. Il peut également évaluer toute formule valide en fonction des valeurs de vérité de ses composants atomiques, et cela indépendamment du sens des atomes composant la formule, il s'agit de tâches purement mécaniques.
Une notion importante est celle de 'sous-formule' , définie récursivement :
Ainsi par exemple:
P, Q, R , ¬ R, P∨Q
sont des sous-formules de (P∨Q)∧(¬ R)
La notion de 'substitution' est liée à la notion précédente:
Si G est une formule admettant H pour sous-formule G:H/K est une formule obtenue par remplacement de H par K dans G.
Ainsi si G=(P∨Q)∧(¬ R) et si H=P∨Q
G:H/S=S∧(¬ R)

Café Python

Voici un premier programme qui effectue une analyse syntaxique pour reconnaître les formules correctement formées.

Voici un second programme qui évalue une formule du calcul propositionnel.

Voici un troisième programme qui évalue une formule du calcul propositionnel, en utilisant les modules lex et yacc (module python ply)