Vitor Greati

Learn how to implement bilateralism via a two-dimensional notion of consequence, actualized by a two-dimensional notion of logical matrices and a two-dimensional Hilbert-style proof formalism. Automatically generate two-dimensional analytic calculi for sufficiently expressive two-dimensional matrices and do proof search over the resulting systems. If you have luck, your favorite logic may live inside a two-dimensional consequence induced by an analytic calculus, and you may even discover, just by looking at the rules of inference, that it is polynomial-time decidable!