alphabet (des symboles)

Renault
Peugeot
Ford
Citroën
Marque
Modèle
R5
Clio
Névada
206 coupé
307 familial
2CV
Fiesta
Berline
Break
Coupé
(
)
non //(négation)
^ //(et, ou conjonction)
-> //(implique)
v //(ou, ou disjonction)

procédé de formation des expressions
expression <= symbole
expression <= ( expression )
expression <= non expression
expression <= expression1 ^ expression2
expression <= expression1 v expression2
expression <= expression1 -> expression2

axiomes
R1 : (Clio v R5 v Névada) -> Renault
R2 : (206 Coupé v 307 familial) -> Peugeot
R3 : (2CV) -> Citroën
R4 : (Fiesta) -> Ford
R5 : (Névada v 307 familial) -> break
R6 : (R5 v Clio v 2CV)-> berline
R7 : (206 coupé) ->Coupé

règle de dérivation (Cette règle est connue sous le nom de "modus ponens" )

Si A est un théorème, et si
A -> B est un théorème, alors
B est un théorème