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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Schematic Reasoning in GAPT

  • Alexander Leitsch,
  • David Michael Cerna,
  • Anela Lolic

摘要

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.