English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

This article describes an evaluation of Automated Theorem Proving (ATP)systems on problems taken from the QMLTP library of first-order modal logicproblems. Principally, the problems are translated to both typed first-orderand higher-order logic in the TPTP language using an embedding approach, andsolved using first-order resp. higher-order logic ATP systems and modelfinders. Additionally, the results from native modal logic ATP systems areconsidered, and compared with the results from the embedding approach. Thefindings are that the embedding process is reliable and successful whenstate-of-the-art ATP systems are used as backend reasoners, The first-order andhigher-order embeddings perform similarly, native modal logic ATP systems havecomparable performance to classical systems using the embedding for provingtheorems, native modal logic ATP systems are outperformed by the embeddingapproach for disproving conjectures, and the embedding approach can cope with awider range of modal logics than the native modal systems considered.

Solving Quantified Modal Logic Problems by Translation to Classical Logics