JGXYZ - An ATP System for Gap and Glut Logics
Abstract
This talk describes an ATP system, named JGXYZ, for some gap and glut logics.
JGXYZ is based on an equi-provable translation to FOL, followed by use of an
existing ATP system for FOL. A key feature of JGXYZ is that the translation
to FOL is data-driven, in the sense that it requires only the addition of a
new logic's truth tables for the unary and binary connectives in order to
produce an ATP system for the logic. Experimental results from JGXYZ illustrate
the differences between the logics and translated problems, both technically
and in terms of a quasi-real-world use case.