•  1
    Engaged in Relations: A Trialogue
    with Michał Zawidzki and Ewa Orłowska
    In Michał Zawidzki & Joanna Golińska-Pilarek (eds.), Ewa Orłowska on Relational Methods in Logic and Computer Science, Springer Verlag. 2018.
    The chapter is a transcription of editors’ discussion with Ewa Orłowska. It reveals some extracurricular flavors of Ewa Orłowska’s biography, brings to light a difficult historical context of her academic career and life, and shows how much internal fortitude she demonstrated while overcoming these difficulties.
  •  2
    Everything is a Relation: A Preview
    In Michał Zawidzki & Joanna Golińska-Pilarek (eds.), Ewa Orłowska on Relational Methods in Logic and Computer Science, Springer Verlag. pp. 3-24. 2018.
    This chapter provides a concise overview of Ewa Orłowska’s research contributions and the content of the volume.
  •  2
    A Mystery of Grzegorczyk’s Logic of Descriptions
    with Taneli Huuskonen
    In Urszula Wybraniec-Skardowska & Ángel Garrido (eds.), The Lvov-Warsaw School. Past and Present, Springer- Birkhauser,. pp. 731-745. 2018.
    In 2011, Andrzej Grzegorczyk formulated Logic of Descriptions, a new logical system in which the classical equivalence has been replaced with the descriptive equivalence. Two sentences are descriptively equivalent whenever they describe the same state of affairs. Grzegorczyk’s logic LD is built from the ground up by revising the axioms of classical propositional logic and rejecting those that do not correspond to the intended interpretation of the descriptive equivalence as the connective expres…Read more
  •  5
    A hybrid qualitative approach for relative movements
    with Emilio Muñoz-Velasco
    Logic Journal of the IGPL 23 (3): 410-420. 2015.
    Qualitative description of movements can be very important for representation and reasoning about dynamic systems which are complex in structure or whenever numerical data are incomplete or inaccessible. For this reason, we present a hybrid approach based on the combination of qualitative reasoning, quantitative data and logical methods. In this article, we introduce a new propositional dynamic logic QM for representation and reasoning with relative movements of objects. In this way, we can infe…Read more
  •  13
    Filozofia w Polsce po reformie – szanse i wyzwania
    Ruch Filozoficzny 76 (1): 251. 2020.
  •  12
    This book is a tribute to Professor Ewa Orłowska, a Polish logician who was celebrating the 60th year of her scientific career in 2017. It offers a collection of contributed papers by different authors and covers the most important areas of her research. Prof. Orłowska made significant contributions to many fields of logic, such as proof theory, algebraic methods in logic and knowledge representation, and her work has been published in 3 monographs and over 100 articles in internationally acclai…Read more
  •  6
    Relational dual tableau decision procedures and their applications to modal and intuitionistic logics
    with Taneli Huuskonen
    Annals of Pure and Applied Logic 165 (2): 428-502. 2014.
    This paper introduces Basic Intuitionistic Set Theory BIST, and investigates it as a first-order set theory extending the internal logic of elementary toposes. Given an elementary topos, together with the extra structure of a directed structural system of inclusions on the topos, a forcing-style interpretation of the language of first-order set theory in the topos is given, which conservatively extends the internal logic of the topos. This forcing interpretation applies to an arbitrary elementar…Read more
  •  37
    The book presents logical foundations of dual tableaux together with a number of their applications both to logics traditionally dealt with in mathematics and philosophy (such as modal, intuitionistic, relevant, and many-valued logics) and to various applied theories of computational logic (such as temporal reasoning, spatial reasoning, fuzzy-set-based reasoning, rough-set-based reasoning, order-of magnitude reasoning, reasoning about programs, threshold logics, logics of conditional decisions).…Read more
  •  46
    Relational dual tableaux for interval temporal logics
    with David Bresolin and Ewa Orlowska
    Journal of Applied Non-Classical Logics 16 (3-4). 2006.
    Interval temporal logics provide both an insight into a nature of time and a framework for temporal reasoning in various areas of computer science. In this paper we present sound and complete relational proof systems in the style of dual tableaux for relational logics associated with modal logics of temporal intervals and we prove that the systems enable us to verify validity and entailment of these temporal logics. We show how to incorporate in the systems various relations between intervals an…Read more
  •  41
    A new deduction system for deciding validity in modal logic K
    with Emilio Munoz Velasco and Angel Mora
    Logic Journal of the IGPL 19 (2). 2011.
    A new deduction system for deciding validity for the minimal decidable normal modal logic K is presented in this article. Modal logics could be very helpful in modelling dynamic and reactive systems such as bio-inspired systems and process algebras. In fact, recently the Connectionist Modal Logics has been presented, which combines the strengths of modal logics and neural networks. Thus, modal logic K is the basis for these approaches. Soundness, completeness and the fact that the system itself …Read more
  •  15
    On the Minimal Non-Fregean Grzegorczyk Logic
    Studia Logica 104 (2): 209-234. 2016.
    The paper concerns Grzegorczyk’s non-Fregean logics that are intended to be a formal representation of the equimeaning relation defined on descriptions. We argue that the main Grzegorczyk logics discussed in the literature are too strong and we propose a new logical system, \, which satisfies Grzegorczyk’s fundamental requirements. We present a sound and complete semantics for \ and we prove that it is decidable. Finally, we show that many non-classical logics are extensions of \, which makes it…Read more
  •  37
    Reasoning with Qualitative Velocity: Towards a Hybrid Approach
    with Emilio Munoz Velasco
    In Emilio Corchado, Vaclav Snasel, Ajith Abraham, Michał Woźniak, Manuel Grana & Sung-Bae Cho (eds.), Hybrid Artificial Intelligent Systems, Springer. pp. 635--646. 2012.
    Qualitative description of the movement of objects can be very important when there are large quantity of data or incomplete information, such as in positioning technologies and movement of robots. We present a first step in the combination of fuzzy qualitative reasoning and quantitative data obtained by human interaction and external devices as GPS, in order to update and correct the qualitative information. We consider a Propositional Dynamic Logic which deals with qualitative velocity and ena…Read more
  •  26
    Logics of similarity and their dual tableaux. A survey
    In Giacomo Della Riccia, Didier Dubois & Hans-Joachim Lenz (eds.), Preferences and Similarities, Springer. pp. 129--159. 2008.
    We present several classes of logics for reasoning with information stored in information systems. The logics enable us to cope with the phenomena of incompleteness of information and uncertainty of knowledge derived from such an information. Relational inference systems for these logics are developed in the style of dual tableaux.
  •  54
    Tableaux and Dual Tableaux: Transformation of Proofs
    with Ewa Orłowska
    Studia Logica 85 (3): 283-302. 2007.
    We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We sho…Read more
  •  35
    Number of Extensions of Non-Fregean Logics
    with Taneli Huuskonen
    Journal of Philosophical Logic 34 (2): 193-206. 2005.
    We show that there are continuum many different extensions of SCI (the basic theory of non-Fregean propositional logic) that lie below WF (the Fregean extension) and are closed under substitution. Moreover, continuum many of them are independent from WB (the Boolean extension), continuum many lie above WB and are independent from WH (the Boolean extension with only two values for the equality relation), and only countably many lie between WH and WF
  •  37
    Relational dual tableau decision procedure for modal logic K
    with Emilio Munoz-Velasco and Angel Mora
    Logic Journal of the IGPL 20 (4): 747-756. 2012.
    We present a dual tableau system, RLK, which is itself a deterministic decision procedure verifying validity of K-formulas. The system is constructed in the framework of the original methodology of relational proof systems, determined only by axioms and inference rules, without any external techniques. Furthermore, we describe an implementation of the system RLK in Prolog, and we show some of its advantages.
  •  29
    We present a relational proof system in the style of dual tableaux for the relational logic associated with a multimodal propositional logic for order of magnitude qualitative reasoning with a bidirectional relation of negligibility. We study soundness and completeness of the proof system and we show how it can be used for verification of validity of formulas of the logic.
  •  21
    Relational dual tableau decision procedures and their applications to modal and intuitionistic logics
    with Taneli Huuskonen and Emilio Muñoz-Velasco
    Annals of Pure and Applied Logic 165 (2): 409-427. 2014.
    This paper introduces Basic Intuitionistic Set Theory BIST, and investigates it as a first-order set theory extending the internal logic of elementary toposes. Given an elementary topos, together with the extra structure of a directed structural system of inclusions on the topos, a forcing-style interpretation of the language of first-order set theory in the topos is given, which conservatively extends the internal logic of the topos. This forcing interpretation applies to an arbitrary elementar…Read more
  •  154
    Spectra of formulae with Henkin quantifiers
    with Konrad Zdanowski
    In A. Rojszczak, J. Cachro & G. Kurczewski (eds.), Philosophical Dimensions of Logic and Science, Kluwer Academic Publishers. pp. 29-45. 2003.
    It is known that various complexity-theoretical problems can be translated into some special spectra problems. Thus, questions about complexity classes are translated into questions about the expressive power of some languages. In this paper we investigate the spectra of some logics with Henkin quantifiers in the empty vocabulary.
  •  10
    On Decidability of a Logic for Order of Magnitude Qualitative Reasoning with Bidirectional Negligibility
    In Luis Farinas del Cerro, Andreas Herzig & Jerome Mengin (eds.), Logics in Artificial Intelligence, Springer. pp. 255--266. 2012.
    Qualitative Reasoning (QR) is an area of research within Artificial Intelligence that automates reasoning and problem solving about the physical world. QR research aims to deal with representation and reasoning about continuous aspects of entities without the kind of precise quantitative information needed by conventional numerical analysis techniques. Order-of-magnitude Reasoning (OMR) is an approach in QR concerned with the analysis of physical systems in terms of relative magnitudes. In this …Read more
  •  26
    Number of non-Fregean sentential logics that have adequate models
    Mathematical Logic Quarterly 52 (5). 2006.
    We show that there are continuum many different non-Fregean sentential logics that have adequate models. The proof is based on the construction of a special class of models of the power of the continuum.
  •  23
    Relational proof systems for spatial reasoning
    Journal of Applied Non-Classical Logics 16 (3-4): 409-431. 2006.
    We present relational proof systems for the four groups of theories of spatial reasoning: contact relation algebras, Boolean algebras with a contact relation, lattice-based spatial theories, spatial theories based on a proximity relation
  •  13
    Dual tableau for monoidal triangular norm logic MTL
    Fuzzy Sets and Systems 162 (1). 2011.
    Monoidal triangular norm logic MTL is the logic of left-continuous triangular norms. In the paper we present a relational formalization of the logic MTL and then we introduce relational dual tableau that can be used for verification of validity of MTL-formulas. We prove soundness and completeness of the system.
  •  26
    Relational dual tableau decision procedure for modal logic K
    with Emilio Muñoz-Velasco and Angel Mora-Bonilla
    Logic Journal of the IGPL 20 (4): 747-756. 2012.
    We present a dual tableau system, RLK, which is itself a deterministic decision procedure verifying validity of K-formulas. The system is constructed in the framework of the original methodology of relational proof systems, determined only by axioms and inference rules, without any external techniques. Furthermore, we describe an implementation of the system in Prolog, and we show some of its advantages.
  •  29
    Implementing a relational theorem prover for modal logic K
    with Angel Mora and Emilio Munoz Velasco
    International Journal of Computer Mathematics 88 (9): 1869-1884. 2011.
    An automatic theorem prover for a proof system in the style of dual tableaux for the relational logic associated with modal logic K has been introduced. Although there are many well-known implementations of provers for modal logic, as far as we know, it is the first implementation of a specific relational prover for a standard modal logic. There are two main contributions in this paper. First, the implementation of new rules, called (k1) and (k2), which substitute the classical relational rules …Read more
  •  22
    We present a relational proof system in the style of dual tableaux for a multimodal propositional logic for order of magnitude qualitative reasoning to deal with relations of negligibility, non-closeness, and distance. This logic enables us to introduce the operation of qualitative sum for some classes of numbers. A relational formalization of the modal logic in question is introduced in this paper, i.e., we show how to construct a relational logic associated with the logic for order-of-magnitud…Read more
  •  49
    An ATP of a Relational Proof System for Order of Magnitude Reasoning with Negligibility, Non-closeness and Distance
    with Angel Mora and Emilio Munoz Velasco
    In Tu-Bao Ho & Zhi-Hua Zhou (eds.), PRICAI 2008: Trends in Artificial Intelligence, Springer. pp. 128--139. 2008.
    We introduce an Automatic Theorem Prover (ATP) of a dual tableau system for a relational logic for order of magnitude qualitative reasoning, which allows us to deal with relations such as negligibility, non-closeness and distance. Dual tableau systems are validity checkers that can serve as a tool for verification of a variety of tasks in order of magnitude reasoning, such as the use of qualitative sum of some classes of numbers. In the design of our ATP, we have introduced some heuristics, such…Read more
  •  30
    Non-Fregean Propositional Logic with Quantifiers
    with Taneli Huuskonen
    Notre Dame Journal of Formal Logic 57 (2): 249-279. 2016.
    We study the non-Fregean propositional logic with propositional quantifiers, denoted by $\mathsf{SCI}_{\mathsf{Q}}$. We prove that $\mathsf{SCI}_{\mathsf{Q}}$ does not have the finite model property and that it is undecidable. We also present examples of how to interpret in $\mathsf{SCI}_{\mathsf{Q}}$ various mathematical theories, such as the theory of groups, rings, and fields, and we characterize the spectra of $\mathsf{SCI}_{\mathsf{Q}}$-sentences. Finally, we present a translation of $\math…Read more
  •  40
    Rasiowa-Sikorski proof system for the non-Fregean sentential logic SCI
    Journal of Applied Non-Classical Logics 17 (4). 2007.
    The non-Fregean logic SCI is obtained from the classical sentential calculus by adding a new identity connective = and axioms which say ?a = ß' means ?a is identical to ß'. We present complete and sound proof system for SCI in the style of Rasiowa-Sikorski. It provides a natural deduction-style method of reasoning for the non-Fregean sentential logic SCI