JGXYZ - An ATP System for Gap and Glut Logics

Background and Motivation

• Automated Reasoning
• Classical First-order Logic
• The Need for More Truth Values
• The Truth and Information Diamonds

Gap and Glut Logics

• The Gap Logic Ł3
• The Glut Logic RM3
• Belnap's Gap and Glut Logic FDE (without a conditional)
  • Classical implication - a bad idea
  • Classical material implication (→_cmi)
  • The "Łukasiewicz" conditional (→_Ł3)
• Five Gap and Glut Logics

System Implementation

• Indirect Proofs
• The Translational Approach
• The Truth Evaluation Approach
• JGXYZ Implementation

Evaluation

• The Motivating Example
• Illustrative Examples

Conclusion

The End - Any Questions?