Conclusion

Contribution

• System using classical first-order ATP in KBR
• Demonstration that KBR can absolve itself of ATP concerns

Application

• Rightscom domain ontology reasoning
• Military Q&A and dialog system

Future Work

• Use of TPTP higher-order (THF) format and ATP systems

The End - Any Questions?