A simplified version of the Sequent Calculus G3[mic]^=
Logic
2018-10-29 v1
Abstract
We show that the Replacement Rule in the sequent calculus G3[mic]}^=, for first order languages with function symbols and equality, can be replaced by the simpler rule in which the transformed formula is not repeated in the premiss.
Cite
@article{arxiv.1810.11355,
title = {A simplified version of the Sequent Calculus G3[mic]^=},
author = {Franco Parlamento and Flavio Previale},
journal= {arXiv preprint arXiv:1810.11355},
year = {2018}
}
Comments
10 pages