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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Proof assistants often call automated theorem provers to prove subgoals.However, each prover has its own proof calculus and the proof traces that itproduces often lack many details to build a complete proof. Hence these tracesare hard to check and reuse in proof assistants. Dedukti is a proof checkerwhose proofs can be translated to various proof assistants: Coq, HOL, Lean,Matita, PVS. We implemented a tool that extracts TPTP subproblems from a TSTPfile and reconstructs complete proofs in Dedukti using automated provers ableto generate Dedukti proofs like ZenonModulo or ArchSAT. This tool is generic:it assumes nothing about the proof calculus of the prover producing the trace,and it can use different provers to produce the Dedukti proof. We applied ourtool on traces produced by automated theorem provers on the CNF problems of theTPTP library and we were able to reconstruct a proof for a large proportion ofthem, significantly increasing the number of Dedukti proofs that could beobtained for those problems.

EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)