Title: Computations in Fragments of Intuitionistic Propositional Logic
Abstract: This article is a report on research in progress into the structure of finite diagrams of intuitionistic propositional logic with the aid of automated reasoning systems for larger calculations. A fragment of a propositional logic is the set of formulae built up from a finite number of propositional variables by means of a number of connectives of the logic, among which possibly non-standard ones like ¬¬ or ↔ which are studied here. The diagram of that fragment is the set of equivalence classes of its formulae partially ordered by the derivability relation. A concept of exact model has been used to construct subdiagrams of the [p, q, ^, →, ¬]-fragment.
Publication Year: 1991
Publication Date: 1991-01-01
Language: en
Type: article
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot