JGXYZ: An ATP system for gap and glut logics

Geoff Sutcliffe, Francis Jeffry Pelletier

Research output: Chapter in Book/Report/Conference proceedingConference contribution


This paper 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.

Original languageEnglish (US)
Title of host publicationAutomated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings
EditorsPascal Fontaine
Number of pages12
ISBN (Print)9783030294359
StatePublished - 2019
Event27th International Conference on Automated Deduction, CADE 2019 - Natal, Brazil
Duration: Aug 27 2019Aug 30 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11716 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference27th International Conference on Automated Deduction, CADE 2019


  • ATP system
  • Gap logic
  • Glut logic
  • Multi-valued logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'JGXYZ: An ATP system for gap and glut logics'. Together they form a unique fingerprint.

Cite this