Schematic Reasoning in GAPT
摘要
Rather than developing a system from scratch, we integrated our interactive system for schematic proof analysis with schematic CERES within the software package GAPT (General Architecture for Proof Theory) (Ebner et al. in International joint conference on automated reasoning, pp 293–301 (2016), [16]). The GAPT system provides numerous algorithms for the analysis, transformation, and construction of proofs in various formal calculi and has been used for CERES based proof analysis. GAPT is implemented in Scala and licensed under the GNU General Public License.