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 develop combinatorial test generation algorithms for progressively morepowerful theorem provers, covering formula languages ranging from theimplicational fragment of intuitionistic logic to full intuitionisticpropositional logic. Our algorithms support exhaustive and random generatorsfor formulas of these logics.  To provide known-to-be-provable formulas, via the Curry-Howardformulas-as-types correspondence, we use generators for typable lambda termsand combinator expressions. Besides generators for several classes of formulas,we design algorithms that restrict formula generation to canonicalrepresentatives among equiprovable formulas and introduce programtransformations that reduce formulas to equivalent formulas of a simplerstructure. The same transformations, when applied in reverse, create harderformulas that can catch soundness or incompleteness bugs.  To test the effectiveness of the testing framework itself, we describe usecases for deriving lightweight theorem provers for several of these logics andfor finding bugs in known theorem provers. Our Prolog implementation availableat: https://github.com/ptarau/TypesAndProofs and a subset of formula generatorsand theorem provers, implemented in Python is available at:https://github.com/ptarau/PythonProvers.  Keywords: term and formula generation algorithms, Prolog-based theoremprovers, formulas-as-types, type inference and type inhabitation, combinatorialtesting, finding bugs in theorem provers.

Formula Transformers and Combinatorial Test Generators for Propositional Intuitionistic Theorem Provers