Application Préservant les Conséquences

Une transformation entre systèmes syntaxiques, ensembles de formules ou modèles qui préserve la conséquence logique : chaque fois qu’une formule découle d’un ensemble de prémisses dans la source (Γ ⊨ φ ou Γ ⊢ φ), les images de ces prémisses entraînent l’image de la conclusion dans la cible (mapped(Γ) ⊨ mapped(φ) ou mapped(Γ) ⊢ mapped(φ)).