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

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 monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Basic proof-search tactics in logic and type theory can be seen as theroot-first applications of rules in an appropriate sequent calculus, preferablywithout the redundancies generated by permutation of rules. This paperaddresses the issues of defining such sequent calculi for Pure Type Systems(PTS, which were originally presented in natural deduction style) and thenorganizing their rules for effective proof-search. We introduce the idea ofPure Type Sequent Calculus with meta-variables (PTSCalpha), by enriching thesyntax of a permutation-free sequent calculus for propositional logic due toHerbelin, which is strongly related to natural deduction and already welladapted to proof-search. The operational semantics is adapted from Herbelin'sand is defined by a system of local rewrite rules as in cut-elimination, usingexplicit substitutions. We prove confluence for this system. Restricting ourattention to PTSC, a type system for the ground terms of this system, we obtainthe Subject Reduction property and show that each PTSC is logically equivalentto its corresponding PTS, and the former is strongly normalising iff the latteris. We show how to make the logical rules of PTSC into a syntax-directed systemPS for proof-search, by incorporating the conversion rules as insyntax-directed presentations of the PTS rules for type-checking. Finally, weconsider how to use the explicitly scoped meta-variables of PTSCalpha torepresent partial proof-terms, and use them to analyse interactive proofconstruction. This sets up a framework PE in which we are able to studyproof-search strategies, type inhabitant enumeration and (higher-order)unification.

A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems