Synthetic Tableaux with Unrestricted Cut for First-Order Theories
The method of synthetic tableaux is a cut-based tableau system with synthesizing rules introducing complex formulas. In this paper, we present the method of synthetic tableaux for Classical First-Order Logic, and we propose a strategy of extending the system to first-order theories axiomatized by universal axioms. The strategy was inspired by the works of Negri and von Plato. We illustrate the strategy with two examples: synthetic tableaux systems for identity and for partial order.
Keyword(s):
2009 ◽
Vol 19
(12)
◽
pp. 3091-3099
◽
Keyword(s):
2019 ◽
Vol 29
(8)
◽
pp. 1311-1344
◽
Keyword(s):
Keyword(s):