Conclusion

What we Did

• Translate QMLTP to TPTP NTF language
• Embed NTF problems into THF
• Evaluate performance of higher-order ATP on THF problems
• Compare with native modal logic ATP systems

What we Found Out

• The embedding process is reliable and successful
• Choice of THF ATP system significantly impacts performance
• Native modal logic ATP systems outperform embedding approach
• Embedding can cope with a wider range of modal logics

What we Plan to do Next

• Complete embedding for non-constant domains
• Use model finders to disprove non-theorems
• Convert THF proofs (with FOF/PRP parts) to NTF
• Release TPTP v9.0.0 with modal logic problems
• Develop support for NTF in the TPTP World