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

Studies on type theory have brought numerous important contributions to computer science. In this paper we present a GUI-based proof tool that provides assistance in constructing deductions in type theory and validating implicational intuitionistic-logic formulas. As such, this proof tool is a testbed for learning type theory and implicational intuitionistic-logic. This proof tool focuses on an important variant of type theory named TA , especially on its two core algorithms: the principal-type algorithm and the type inhabitant search algorithm. The former algorithm nds a most general type assignable to a given -term, while the latter nds inhabitants (closed -terms in -normal form) to which a given type can be assigned. By the Curry{Howard correspondence, the latter algorithm provides provability for implicational formulas in intuitionistic logic. We elaborate on how to implement those two algorithms declaratively in Prolog and the overall GUI-based program architecture. In our implementation, we make some modication to improve the performance of the principal-type algorithm. We have also built a web-based version of the proof tool called -Guru.

A Prolog-based Proof Tool for Type-Theory TA-lambda and Implicational Intuitionistic-Logic