Возникает еще одна формальная сложность: процесс логического вывода, в котором используются эти аксиомы, должен позволять доказывать неравенства. Простейшего рода неравенство задается между константами, например Agent^G^ Общая семантика логики первого порядка допускает, чтобы разные константы ссылались на один и тот же объект, поэтому база знаний должна включать какую-то аксиому, позволяющую предотвратить такую ситуацию. В ^ аксиоме уникальных имен (unique names axiom) провозглашается неравенство для каждой пары констант в базе знаний. Если же это условие подразумевается в программе автоматического доказательства теорем, а не записывается в базу знаний, то называется предположением об уникальности имен (unique names assumption). Необходимо также сформулировать условие неравенства между термами действий, например, утверждение о том, что Go ([1,1], [1,2])— это действие, отличное от Go ( [ 1, 2 ] , [ 1,1 ] ) или Grab (G1). Прежде всего необходимо указать, что каждый тип действия является различным, т.е., например, что действие Go — это не действие Grab. Для каждой пары имен действий А и B необходимо иметь:

Затем требуется указать, что два терма действия с одним и тем же именем действия ссылаются на одно и то же действие тогда и только тогда, когда все участвующие в них объекты являются одинаковыми:

Все эти аксиомы, вместе взятые, называются аксиомами уникального действия (unique action axiom). Такая комбинация описания начального состояния, аксиом состояния-преемника, аксиом уникальности имен и аксиом уникального действия является достаточной для доказательства того, что предлагаемый план позволяет достичь цели.