Podle mě prázdnou klauzuli z b != b pravidly rezoluce, faktorizace a paramodulace bez použití axiomu reflexivity neodvodíte. Důvod je jednoduchý - žádné z těch pravidel nejde použít.
Lze ale reflexivitu spojit s rezolucí a udělat pravidlo (s != t ⋁ R) → Rσ, kde σ = mgu(s, t).
Ještě jedna poznámka - u axiomů rovnosti vám chybí schémata kongruence.
ČLÁNKY DO MAILU