Abstract
A system with variable splitting is introduced for a sequent calculus with free variables and run-time Skolemization. Derivations in the system are invariant under permutation, so that the order in which rules are applied has no effect on the leaves. Technically this is achieved by means of a simple indexing system for formulae, variables and Skolem functions. Moreover, the way in which variables are split enables us to restrict the term universe branchwise.
Cite
CITATION STYLE
Waaler, A., & Antonsen, R. (2003). A free variable sequent calculus with uniform variable splitting. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2796, pp. 214–229). Springer Verlag. https://doi.org/10.1007/978-3-540-45206-5_17
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
