This paper describes an evaluation of Automated Theorem Proving (ATP) systems on problems taken from the QMLTP library of first-order modal logic problems. Principally, the problems are translated to higher-order logic in the TPTP language using an embedding approach, and solved using higher-order logic ATP systems. Additionally, the results from native modal logic ATP systems are considered, and compared with those from the embedding approach. The findings are that the embedding process is reliable and successful, the choice of backend ATP system can significantly impact the performance of the embedding approach, native modal logic ATP systems outperform the embedding approach, and the embedding approach can cope with a wider range modal logics than the native modal systems considered.

This paper reports on an exploration of Boolos' Curious Inference, using higher-order automated theorem provers (ATPs). Surprisingly, only suitable shorthand notations had to be provided by hand for ATPs to find a short proof. The higher-order lemmas required for constructing a short proof are automatically discovered by the ATPs. Given the observations and suggestions in this paper, full proof automation of Boolos' and related examples now seems to be within reach of higher-order ATPs.

The CADE ATP System Competition (CASC) is an annual evaluation of fully automatic automated theorem proving (ATP) systems for classical logic — the world championship for such systems. CASC provides a public evaluation of the relative capabilities of ATP systems, and aims stimulate ATP research towards the development of more powerful ATP systems. Over the years CASC has been a catalyst for impressive improvements in ATP.

The Semantic Web ontology language OWL 2 DL comes with a variety of language features that enable sophisticated and practically useful modeling. However, the use of these features has been severely restricted in order to retain decidability of the language. For example, OWL 2 DL does not allow a property to be both transitive and asymmetric, which would be desirable, e.g., for representing an ancestor relation. In this paper, we argue that the so-called global restrictions of OWL 2 DL preclude many useful forms of modeling, by providing a catalog of basic modeling patterns that would be available in OWL 2 DL if the global restrictions were discarded. We then report on the results of evaluating several state-of-the-art OWL 2 DL reasoners on problems that use combinations of features in a way that the global restrictions are violated. The systems turn out to rely heavily on the global restrictions and are thus largely incapable of coping with the modeling patterns. Next we show how off-the-shelf first-order logic theorem proving technology can be used to perform reasoning in the OWL 2 direct semantics, the semantics that underlies OWL 2 DL, but without requiring the global restrictions. Applying a naive proof-of-concept implementation of this approach to the test problems was successful in all cases. Based on our observations, we make suggestions for future lines of research on expressive description logic-style OWL reasoning.

OWL 2 has been standardized by the World Wide Web Consortium (W3C) as a family of ontology languages for the Semantic Web. The most expressive of these languages is OWL 2 Full, but to date no reasoner has been implemented for this language. Consistency and entailment checking are known to be undecidable for OWL 2 Full. We have translated a large fragment of the OWL 2 Full semantics into first-order logic, and used automated theorem proving systems to do reasoning based on this theory. The results are promising, and indicate that this approach can be applied in practice for effective OWL reasoning, beyond the capabilities of current Semantic Web reasoners. This is an extended version of a paper with the same title that has been published at CADE 2011, LNAI 6803, pp. 446-460. The extended version provides appendices with additional resources that were used in the reported evaluation.

The special tracks chair was Barry O'Sullivan, FLAIRS Conference (FLAIRS-19) was Reversals via Representational Refinements"; held 11-13 May 2006 at the Crowne Bob Morris of the NASA Ames The 20th International FLAIRS Conference (FLAIRS-20) will be held May 7 - 9, 2007 at the Casa Marina Resort, which is directly on the beach in Key West, Florida, USA. FLAIRS-20 will feature technical papers, special tracks, and invited speakers on artificial intelligence. The conference is hosted by the Florida Artificial Intelligence Research General Chair Society, in cooperation with AAAI. Geoff Sutcliffe In addition to the general conference, FLAIRS offers numerous special conference tracks. Special tracks provide researchers in focused areas the opportunity to meet and present University of Miami their work.

Automated Theorem Proving: A Review

Thus, the reader is able to experiment is a logical consequence of a set of aspects of the deduction steps as both a user and a developer statements (the axioms and hypotheses).