Aura

Rövid szöveges bemutatás: 
Az AURA nevű tételbizonyító programot Wos és Winker alkotta meg 1983-ban. Matematikai kérdésekre kutatta a választ. A működési alapja az ítéletlogika volt. Sikerrel alkalmazták különféle területek például hardverszintézis, ahol olyan áramköröket előállító terveket alkotott, melyek sokkal tömörebbek voltak elődeiknél.