これは数千年に及ぶ人類の叡智である論理学の成果をプログラム言語に置き換えたものと言えるが、現在のでプログラムの制御に使われるカットオペレータに相当する機能が最初から導入されるなど、現在のと同様、単なる定理証明システムではなくプログラミング言語として設計されたものだった。