Miután logikai tételbizonyításokkal procedurálisan (de nem logikailag!) ekvivalens programok végrehajtása a Prolog nyelv tárgya, így a nyelvi helyességbizonyítás szükségtelen - mivel a feladat megfogalmazása logikai axiómák és tételek formájában, majd annak transzformációja standard Prolog notációra a helyességbizonyításon alapul.