Computations in Fragments of Intuitionistic Propositional Logic

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.