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

We propose an automated deduction method which allows us to produce proofsclose to the human intuition and practice. This method is based on tableaux,which generate more natural proofs than similar methods relying on clausalforms, and uses the principles of superdeduction, among which the theory isused to enrich the deduction system with new deduction rules. We present twoimplementations of this method, which consist of extensions of the Zenonautomated theorem prover. The first implementation is a version dedicated tothe set theory of the B formal method, while the second implementation is ageneric version able to deal with any first order theory. We also provideseveral examples of problems, which can be handled by these tools and whichcome from different theories, such as the B set theory or theories of the TPTPlibrary.

Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction