Anwendungen

Für jede Σ mathend000#-Algebra S mathend000# gilt:

• Formel F mathend000# ist allgemeingültig in der freien Σ mathend000#-Algebra
• ⇒ mathend000# Formel F mathend000# ist allgemeingültig in S mathend000#.

Vorteil: kein Entscheidungsverfahren für S mathend000# nötig

Nachteil: Umkehrung gilt nicht.

Anwendung bei Analyse von Programmen, Schaltkreisen: Unterprogramme (Teilschaltungen) als black box,

Roope Kaivola et al.: Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation, Conf. Computer Aided Verification 2009, http://dx.doi.org/10.1007/978-3-642-02658-4_32