EQP

Kapcsolódó fogalmak: 
elsőrendű logika
Kapcsolódó fogalmak: 
OTTER tételbizonyító
Rövid szöveges bemutatás: 
Az EQP-t (Equational Prover) William McCune hozta létre 1997-ben. Ez egy automata tétel bizonyító, az OTTER egyik változata volt, amelynek alapja az elsőrendű logika. Egy jól implementált, jól működő rendszer volt. Sokfajta technikát használt a szükséges bizonyításokhoz és gyorsan dolgozott. Ismerte az egyesítés műveletét is. Ma már forráskódja és leírása teljesen nyilvános.
Kapcsolódó linkek: 
EQP