Analytic sequent calculi with nonlogical axioms

В этой статье исследуются различные исчисления секвенций включая субструктурные и исчисления с равенством, которые могут использоваться для характеризации систем ИИ. Эти исчисления имеют правила введения логических связок определенной формы и содержат нелогические аксиомы. Нелогические аксиомы представляют знания о предметной области. Выводы в этих исчисления могут быть ограничены нормальной формой и упорядоченной формой. Эти формы накладывают ограничения на использование правил вывода. Доказано, что эти исчисления аналитические. Бесконечного ветвления можно избежать в процедурах вывода для этих исчислений. Библ. – 38 назв.