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/

Global: Zendy Plus annual

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

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

CD Tools is a Prolog library for experimenting with condensed detachment infirst-order ATP, which puts a recent formal view centered around proofstructures into practice. From the viewpoint of first-order ATP, condenseddetachment offers a setting that is relatively simple but with essentialfeatures and serious applications, making it attractive as a basis fordeveloping and evaluating novel techniques. CD Tools includes specializedprovers based on the enumeration of proof structures. We focus here on one ofthese, SGCD, which permits to blend goal- and axiom-driven proof search inparticularly flexible ways. In purely goal-driven configurations it actssimilarly to a prover of the clausal tableaux or connection method family. Inblended configurations its performance is much stronger, close tostate-of-the-art provers, while emitting relatively short proofs. Experimentsshow characteristics and application possibilities of the structure generatingapproach realized by that prover. For a historic problem often studied in ATPit produced a new proof that is much shorter than any known one.

CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)