A focused sequent calculus framework for proof search in pure type systems

DOI10.2168/LMCS-7(1:6)2011zbMATH Open1218.03010arXiv1012.3372MaRDI QIDQ3003307FDOQ3003307

Authors: Stéphane Lengrand, Roy Dyckhoff, James McKinna 

Publication date: 26 May 2011

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: Basic proof-search tactics in logic and type theory can be seen as the root-first applications of rules in an appropriate sequent calculus, preferably without the redundancies generated by permutation of rules. This paper addresses the issues of defining such sequent calculi for Pure Type Systems (PTS, which were originally presented in natural deduction style) and then organizing their rules for effective proof-search. We introduce the idea of Pure Type Sequent Calculus with meta-variables (PTSCalpha), by enriching the syntax of a permutation-free sequent calculus for propositional logic due to Herbelin, which is strongly related to natural deduction and already well adapted to proof-search. The operational semantics is adapted from Herbelin's and is defined by a system of local rewrite rules as in cut-elimination, using explicit substitutions. We prove confluence for this system. Restricting our attention to PTSC, a type system for the ground terms of this system, we obtain the Subject Reduction property and show that each PTSC is logically equivalent to its corresponding PTS, and the former is strongly normalising iff the latter is. We show how to make the logical rules of PTSC into a syntax-directed system PS for proof-search, by incorporating the conversion rules as in syntax-directed presentations of the PTS rules for type-checking. Finally, we consider how to use the explicitly scoped meta-variables of PTSCalpha to represent partial proof-terms, and use them to analyse interactive proof construction. This sets up a framework PE in which we are able to study proof-search strategies, type inhabitant enumeration and (higher-order) unification.

Full work available at URL: https://arxiv.org/abs/1012.3372

Recommendations

• A Sequent Calculus for Type Theory
• Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
• scientific article; zbMATH DE number 65536
• Pure type systems with explicit substitutions
• scientific article; zbMATH DE number 1231701

zbMATH Keywords

type theorysequent calculusPTSstrong normalisationmetavariablesinteractive proof constructionproof-search

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07)

Cited In (10)

• Fiat: deductive synthesis of abstract data types in a proof assistant
• Title not available (Why is that?)
• A Sequent Calculus for Type Theory
• Search algorithms in type theory
• Proof search algorithm in pure logical framework
• Practical Proof Search for Coq by Type Inhabitation
• A cut-free sequent calculus for pure type systems verifying the structural rules of Gentzen/Kleene
• Proof-search in type-theoretic languages: An introduction
• Title not available (Why is that?)
• Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture

Uses Software

• Coq
• HOL
• Automath
• LEGO

This page was built for publication: A focused sequent calculus framework for proof search in pure type systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3003307)