Proof search algorithm in pure logical framework

DOI10.33048/SEMI.2020.17.073MaRDI QIDQ779163zbMATH OpenOpenAlexFDO

Authors D. Yu. Vlasov

Publication date 21 July 2020

Published in Sibirskie Elektronnye Matematicheskie Izvestiya (Search for Journal in Brave)

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

zbMATH Keywords

automated deductionlogical framework

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: By a pure logical framework we mean a framework which does not rely on any particular formal calculus. For example, Metamath is an instance of a pure logical framework. Another example is the Russell system (https://github.com/dmitry-vlasov/russell). In this paper, we describe the proof search algorithm used in Russell. The algorithm is proved to be correct and complete, i.e. it gives only valid proofs and any valid proof can be found (up to a substitution) by the proposed algorithm.

Recommendations

• A focused sequent calculus framework for proof search in pure type systems
• The Twelf Proof Assistant
• scientific article; zbMATH DE number 1354109
• Proof finding algorithms for implicational logics
• Proof Search and Counter Model of Positive Minimal Predicate Logic

Cites work

• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• A Mechanical Proof Procedure and its Realization in an Electronic Computer
• Equality reasoning in sequent-based calculi
• Formal Reductions of the General Combinatorial Decision Problem
• Term indexing

Cited in

(5)

• scientific article; zbMATH DE number 782043 (Why is no real title available?)
• scientific article; zbMATH DE number 915924 (Why is no real title available?)
• Constructive decision via redundancy-free proof-search
• Formal Techniques for Deriving Binary Search Algorithms
• scientific article; zbMATH DE number 2090535 (Why is no real title available?)

Describes a project that uses

Uses Software

• GitHub
• Russell
• Metamath

This page was built for publication: Proof search algorithm in pure logical framework

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