This paper offers a brief analysis of the unification problem in modal transitive logics related to the logic S4 : S4 itself, K4, Grz and Gödel-Löb provability logic GL . As a result, new, but not the first, algorithms for the construction of ‘best’ unifiers in these logics are being proposed. The proposed algorithms are based on our earlier approach to solve in an algorithmic way the admissibility problem of inference rules for S4 and Grz . The first algorithms for (...) the construction of ‘best’ unifiers in the above mentioned logics have been given by S. Ghilardi in [ 16 ]. Both the algorithms in [ 16 ] and ours are not much computationally efficient. They have, however, an obvious significant theoretical value a portion of which seems to be the fact that they stem from two different methodological approaches. (shrink)

We study unification problem and problem of admissibility for inference rules in minimal Johanssonsʼ logic J and positive intuitionistic logic IPC+. This paper proves that the problem of admissibility for inference rules with coefficients is decidable for the paraconsistent minimal Johanssonsʼ logic J and the positive intuitionistic logic IPC+. Using obtained technique we show also that the unification problem for these logics is also decidable: we offer algorithms which compute complete sets of unifiers for any unifiable formula. Checking just unifiability (...) of formulas with coefficients also works via verification of admissibility. (shrink)

We prove that the unification type of Łukasiewicz logic and of its equivalent algebraic semantics, the variety of MV-algebras, is nullary. The proof rests upon Ghilardiʼs algebraic characterisation of unification types in terms of projective objects, recent progress by Cabrer and Mundici in the investigation of projective MV-algebras, the categorical duality between finitely presented MV-algebras and rational polyhedra, and, finally, a homotopy-theoretic argument that exploits lifts of continuous maps to the universal covering space of the circle. We discuss the background (...) to such diverse tools. In particular, we offer a detailed proof of the duality theorem for finitely presented MV-algebras and rational polyhedra—a fundamental result that, albeit known to specialists, seems to appear in print here for the first time. (shrink)

This paper contains a proof-theoretic account of unification in transitive reflexive modal logics, which means that the reasoning is syntactic and uses as little semantics as possible. New proofs of theorems on unification types are presented and these results are extended to negationless fragments. In particular, a syntactic proof of Ghilardi’s result that $\mathsf {S4}$ has finitary unification is provided. In this approach the relation between classical valuations, projective unifiers, and admissible rules is clarified.

In this paper we study the admissible rules of intermediate logics. We establish some general results on extensions of models and sets of formulas. These general results are then employed to provide a basis for the admissible rules of the Gabbay–de Jongh logics and to show that these logics have finitary unification type.

Unifiability of terms (and formulas) and structural completeness in the variety of relation algebras RA and in the products of modal logic S5 is investigated. Nonunifiable terms (formulas) which are satisfiable in varieties (in logics) are exhibited. Consequently, RA and products of S5 as well as representable diagonal-free n-dimensional cylindric algebras, RDfn, are almost structurally complete but not structurally complete. In case of S5n a basis for admissible rules and the form of all passive rules are provided.

We characterize all finitary consequence relations over S4.3, both syntactically, by exhibiting so-called passive rules that extend the given logic, and semantically, by providing suitable strongly adequate classes of algebras. This is achieved by applying an earlier result stating that a modal logic L extending S4 has projective unification if and only if L contains S4.3. In particular, we show that these consequence relations enjoy the strong finite model property, and are finitely based. In this way, we extend the known (...) results by Bull and Fine, from logics, to consequence relations. We also show that the lattice of consequence relations over S4.3 is countable and distributive and it forms a Heyting algebra. (shrink)

L.L. Maksimova and L. Esakia, V. Meskhi showed that the modal logic \ has exactly 5 pretabular extensions PM1–PM5. In this paper, we study the problem of unification for all given logics. We showed that PM2 and PM3 have finitary, and PM1, PM4, PM5 have unitary types of unification. Complete sets of unifiers in logics are described.

In this paper, we show that the implication fragment of classical propositional logic is finitary for unification with parameters.

Epistemic logics are essential to the design of logical systems that capture elements of reasoning about knowledge. In this paper, we study the computability of unifiability and the unification types in several epistemic logics.

The product of two |$\textbf {Alt}$| logics possesses the polynomial product finite model property and its membership problem is |$\textbf {coNP}$|-complete. Using a reduction from an undecidable domino-tiling problem, we prove that its admissibility problem is undecidable.

Contact Logics provide a natural framework for representing and reasoning about regions in several areas of computer science. In this paper, we focus our attention on reasoning methods for Contact Logics and address the satisfiability problem and the unifiability problem. Firstly, we give sound and complete tableaux-based decision procedures in Contact Logics and we obtain new results about the decidability/complexity of the satisfiability problem in these logics. Secondly, we address the computability of the unifiability problem in Contact Logics and we (...) obtain new results about the unification type of the unifiability problem in these logics. (shrink)

The problem of unification in a normal modal logic $L$ can be defined as follows: given a formula $\varphi$, determine whether there exists a substitution $\sigma$ such that $\sigma $ is in $L$. In this paper, we prove that for several non-symmetric non-transitive modal logics, there exists unifiable formulas that possess no minimal complete set of unifiers.

It is already known that unifiable formulas in normal modal logic |$\textbf {K}+\square ^{2}\bot $| are either finitary or unitary and unifiable formulas in normal modal logic |$\textbf {Alt}_{1}+\square ^{2}\bot $| are unitary. In this paper, we prove that for all |$d{\geq }3$|⁠, unifiable formulas in normal modal logic |$\textbf {K}+\square ^{d}\bot $| are either finitary or unitary and unifiable formulas in normal modal logic |$\textbf {Alt}_{1}+\square ^{d}\bot $| are unitary.

In the ordinary modal language, KD is the modal logic determined by the class of all serial frames. In this paper, we demonstrate that KD is nullary.

The unification problem in a normal modal logic is to determine, given a formula.

Unification in description logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. The inexpressive description logic EL is of particular interest in this context since, on the one hand, several large biomedical ontologies are defined using EL. On the other hand, unification in EL has been shown to be NP-complete and, thus, of considerably lower complexity than unification in other description logics of similarly restricted expressive power. However, EL allows (...) the use of the top concept, which represents the whole interpretation domain, whereas the large medical ontology SNOMED CT makes no use of this feature. Surprisingly, removing the top concept from EL makes the unification problem considerably harder. More precisely, we will show that unification in EL without the top concept is PSPACE-complete. In addition to the decision problem, we also consider the problem of actually computing EL−⊤-unifiers. (shrink)

We prove that $\textbf {K}5$ and some of its extensions that do not contain $\textbf {K}4$ are of unification type $1$.

Hume’s famous character Cleanthes claims that there is no difficulty in explaining the existence of causal chains with no first cause since in them each item is causally explained by its predecessor. Relying on logico-mathematical resources, we argue for two theses: (1) if the existence of Cleanthes’ chain can be explained at all, it must be explained by the fact that the causal law ruling it is in force, and (2) the fact that such a causal law is in force (...) cannot explain the occurrence of the events in the chain. In order to perform (1), we manage to express in mathematical terms the intuitive idea that indefinitely delayed explanation is ultimately no explanation. In order to achieve (2), we identify a logical relation we can prove to be as strong as the causal relation at issue in the Cleanthes passage, according to a precise notion of strength of relations. (shrink)

Hybrid deduction–refutation systems are deductive systems intended to derive both valid and non-valid, i.e., semantically refutable, formulae of a given logical system, by employing together separate derivability operators for each of these and combining ‘hybrid derivation rules’ that involve both deduction and refutation. The goal of this paper is to develop a basic theory and ‘meta-proof’ theory of hybrid deduction–refutation systems. I then illustrate the concept on a hybrid derivation system of natural deduction for classical propositional logic, for which I (...) show soundness and completeness for both deductions and refutations. (shrink)