In the paper we present a technique for eliminating quantifiers of arbitrary order, in particular of first-order. Such a uniform treatment of the elimination problem has been problematic up to now, since techniques for eliminating first-order quantifiers do not scale up to higher-order contexts and those for eliminating higher-order quantifiers are usually based on a form of monotonicity w.r.t implication (set inclusion) and are not applicable to the first-order case. We make a shift to arbitrary relations “ordering” the underlying universe. (...) This allows us to incorporate background theories into higher-order quantifier elimination methods which, up to now, has not been achieved. The technique we propose subsumes many other results, including the Ackermann's lemma and various forms of fixpoint approaches when the “ordering” relations are interpreted as implication and reveals the common principle behind these approaches. (shrink)

Description logics refer to a family of formalisms concentrated around concepts, roles and individuals. They belong to the most frequently used knowledge representation formalisms and provide a logical basis to a variety of well known paradigms. The main reasoning tasks considered in the area of description logics are those reducible to subsumption. On the other hand, any knowledge representation system should be equipped with a more advanced reasoning machinery. Therefore in the current paper we make a step towards integrating description (...) logics with second-order reasoning. One of the important motivations behind introducing second-order formalism follows from the fact that many forms of commonsense and nonmonotonic reasoning used in AI can be modelled within the second-order logic. To achieve our goal we first extend description logics with a possibility to quantify over concepts. Since one of the main criticisms against the use of second-order formalisms is their complexity, we next propose second-order quantifier elimination techniques applicable to a large class of description logic formulas. Finally we show applications of the techniques, in particular in reasoning with circumscribed concepts and approximated terminological formulas. (shrink)

The paper discusses properties of 4QL, a DATALOG⌉⌉-like query language, originally outlined by Maluszyński and Szalas (Maluszyński & Szalas, 2011). 4QL allows one to use rules with negation in heads and bodies of rules. It is based on a simple and intuitive semantics and provides uniform tools for “lightweight” versions of known forms of nonmonotonic reasoning. Negated literals in heads of rules may naturally lead to inconsistencies. On the other hand, rules do not have to attach meaning to some literals. (...) Therefore 4QL is founded on a four-valued semantics, employing the logic introduced in (Maluszyński et al., 2008; Vitória et al., 2009) with truth values: ‘true’, ‘false’, ‘inconsistent’ and ‘unknown’. In addition, 4QL is tractable w.r.t. data complexity and captures PTIME queries. Even though DATALOG⌉⌉ is known as a concept for the last 30 years, to our best knowledge no existing approach enjoys these properties.In the current paper we:investigate properties of well-supported models of 4QLprove the correctness of the algorithm for computing well-supported modelsshow that 4QL has PTIME data complexity and captures PTIME. (shrink)

Second-order quantifier elimination in the context of classical logic emerged as a powerful technique in many applications, including the correspondence theory, relational databases, deductive and knowledge databases, knowledge representation, commonsense reasoning and approximate reasoning. In the current paper we first generalize the result of Nonnengart and Szałas [17] by allowing second-order variables to appear within higher-order contexts. Then we focus on a semantical analysis of conditionals, using the introduced technique and Gabbay’s semantics provided in [10] and substantially using a third-order (...) accessibility relation. The analysis is done via finding correspondences between axioms involving conditionals and properties of the underlying third-order relation. (shrink)

This paper describes an experimental platform for approximate knowledge databases called the Approximate Knowledge Database, based on a semantics inspired by rough sets. The implementation is based upon the use of a standard SQL database to store logical facts, augmented with several query interface layers implemented in JAVA through which extensional, intensional and local closed world nonmonotonic queries in the form of crisp or approximate logical formulas can be evaluated tractably. A graphical database design user interface is also provided which (...) simplifies the design of databases, the entering of data and the construction of queries. The theory and semantics for AKDBs is presented in addition to application examples and details concerning the database implementation. (shrink)

In the current paper we consider theories with vocabulary containing a number of binary and unary relation symbols. Binary relation symbols represent labeled edges of a graph and unary relations represent unique annotations of the graph's nodes. Such theories, which we call annotation theories^ can be used in many applications, including the formalization of argumentation, approximate reasoning, semantics of logic programs, graph coloring, etc. We address a number of problems related to annotation theories over finite models, including satisfiability, querying problem, (...) specification of preferred models and model checking problem. We show that most of considered problems are NPTime- or co-NPTime-complete. In order to reduce the complexity for particular theories, we use second-order quantifier elimination. To our best knowledge none of existing methods works in the case of annotation theories. We then provide a new second-order quantifier elimination method for stratified theories, which is successful in the considered cases. The new result subsumes many other results, including those of [2, 28, 21]. (shrink)

Mathematical theory of voting and social choice has attracted much attention. In the general setting one can view social choice as a method of aggregating individual, often conflicting preferences and making a choice that is the best compromise. How preferences are expressed and what is the “best compromise” varies and heavily depends on a particular situation. The method we propose in this paper depends on expressing individual preferences of voters and specifying properties of the resulting ranking by means of first-order (...) formulas. Then, as a technical tool, we use methods of second-order quantifier elimination to analyze and compute results of voting. We show how to specify voting, how to compute resulting rankings and how to verify voting protocols. (shrink)

Grammar logics were introduced by Fariñas del Cerro and Penttonen in 1988 and have been widely studied. In this paper we consider regular grammar logics with converse ( REG c logics) and present sound and complete tableau calculi for the general satisfiability problem of REG c logics and the problem of checking consistency of an ABox w.r.t. a TBox in a REG c logic. Using our calculi we develop ExpTime (optimal) tableau decision procedures for the mentioned problems, to which various (...) optimization techniques can be applied. We also prove a new result that the data complexity of the instance checking problem in REG c logics is coNP-complete. (shrink)

Rough Sets were introduced by Z. Pawlak in the year 1982 with the intention to address knowledge representation and data processing from the angle of computation and decision making. The main idea...

In this paper we study automated reasoning in the modal logic CPDLreg which is a combination of CPDL (Propositional Dynamic Logic with Converse) and REGc (Regular Grammar Logic with Converse). The logic CPDL is widely used in many areas, including program verification, theory of action and change, and knowledge representation. On the other hand, the logic REGc is applicable in reasoning about epistemic states and ontologies (via Description Logics). The modal logic CPDLreg can serve as a technical foundation for reasoning (...) about agency. Even very rich multi-agent logics can be embedded into CPDLreg via a suitable translation. Therefore, CPDLreg can serve as a test bed to implement and possibly verify new ideas without providing specific automated reasoning techniques for the logic in question. This process can to a large extent be automated. The idea of embedding various logics into CPDLreg is illustrated on a rather advanced logic TEAMLOGK designed to specify teamwork in multi-agent systems. Apart from defining informational and motivational attitudes of groups of agents, TEAMLOGK allows for grading agents' beliefs, goals and intentions. The current paper is a companion to our paper (Dunin-Kęplicz et al., 2010a). The main contribution are proofs of soundness and completeness of the tableau calculus for CPDLreg provided in (Dunin-Kęplicz et al., 2010a). (shrink)

There are at least two reasons for the wide spread of CAI: 1. that the student is able to control his own process of learning due to immediate evaluation of his work and progress and 2. that evaluation is homogeneous, i.e. independent of subjective fac- tors, which compensates for possible lack of depth. Also, the psychology of man is such that he is less ashamed to be reprimanded for his errors by a machine than by another human being. It is (...) a specic feature of computer aided instruction of logic, particulary the art of proving, that such a system cannot be made other than open. Fortunately, in the case of logic its language makes such a creation possible. An open system is a system that permits arbitrary proof of theorems as long as the former conform to the requirement of a given formal language. The discussed system, Mizar-MSE, evolved, roughly speaking, the above line of thought. It is a natural deduction system practically applied to student instruction. Here I would like to present some of more specic features. (shrink)

First-order logic is formalized by means of tools taken from the logic of questions. A calculus of questions which is a counterpart of the Pure Calculus of Quantifiers is presented. A direct proof of completeness of the calculus is given.

During the global financial crisis of 2007–2009 and the currentCovid-19 debacle, central banks acted quickly, boldly, and effectively. The paper argues that they did so thanks to the lessons learned from the past financial crises, which provided them with opportunities to reconsider their previous beliefs. A case in point is the banking crisis in the United States during the Great Depression of the 1930s that taught central banks to act rapidly and decisively in order to prevent an initial liquidity crisis (...) from escalating into a solvency crisis leading to bankruptcies of banks with potentially disastrous consequences for the entire economy. The paper revisits the consequences of the currency crises of the 1990s, which transformed exchange rate regimes across the world: the EMS one of 1992–1993 that accelerated the launch of the euro, and the Asian one of 1997–1998 resulted in the proliferation of floating exchange rates in emerging economies. (shrink)

The contemporary versions of the ontological argument originated from Charles Hartshorne are formalized proofs (in the metalogical sense of the word) based on unique modal theories. The simplest well-known theory of this kind arises from the system B of modal logic by adding two extra-logical axioms: (AA) “If the perfect being exists, then it necessarily exists” (Anselm’s Axiom) and (AL) “It is possible that the perfect being exists” (Leibniz’s Axiom). In the paper a similar argument is presented, however none of (...) the systems of modal logic is relevant to it. Its only premises are the axiom (AA) and, instead of (AL), the new axiom (AN): “If the perfect being doesn’t exist, it necessarily doesn’t”. The main goal of the work is to prove that (AN) is no more controversial than (AA) and — in consequence — the whole strength of the modal ontological argument lays in the set of its extra-logical premises. In order to do that, three arguments are formulated: ontological, “cosmo­logical” and metalogical. (shrink)

In this paper, I take as a starting point an exchange between Henryk Elzenberg and Roman Ingarden concerning the mode of existence of values. Based on their correspondence, I attempt to trace the missed and lost opportunities for dialogue between the two great Polish axiologists. I demonstrate that while sharing an intense interest in the issue of the existence of values, they addressed them independently and in divergent ways. Following that, I also look at the posthu- mous fate of their (...) unfinished dialogue and argue that their work opens a space for further exploration of the ontology of values. (shrink)

Tekst dotyczy procesu konwersji semantycznej, w wyniku którego sens tradycyjnej koncepcja tolerancji (negatywnej) jest zastępowany przez tak zwaną tolerancje pozytywną. W artykule analizowany jest podmiotowy i przedmiotowy aspekt tolerancji, trudności w pogodzeniu obu koncepcji tolerancji oraz problemy jakie generuje idea tolerancji pozytywnej. Wyróżnione zostały również proste i złożone przedmioty tolerancji.

Political thought of the war and occupation period continued the ideological and program searches started already before 1939. The concept of democracy was mostly associated with the values such as individual freedom, civil rights, safety of citizens, society of the state; cooperation among nations in the fields of politics, economy and protection of peace. The author deals with topics like: democratic international order; democratic political order and economic system. The author concludes the article with a few synthesizing remarks.

The article presents the philosophical thought of Rudolf Zocher, Wolfgang Cramer and Hans Wagner, whose theoretical stance can be dubbed Neoneo-Kantianism. The article investigates their philosophical output and argues that they developed a transcendental reflection of a different kind than that of Baden Neo-Kantianism. The transcendental reflection of Neoneo-Kantianism, especially in the work of Hans Wagner, takes on the topic of phenomenological inquiry and treats consciousness as a source of subject- object distinction, unlike Rickert and Windelband, who were developing transcendental (...) reflection focused on aprioristic forms of cognition, much in the post-Fichtean vein, thus giving primacy to the subjective conditions of possible experience. (shrink)

Quantum mechanics implies many paradoxes (e.g. Schrödinger's cat, double-slit experiment, non-locality) which are in contradiction to our ordinary experience. To comprehend quantum theory we must revise our understanding of such matters as the objective nature of reality, the nature of causality, and the nature of a complex system and its relation to its components. Finally, common sense seems to be an epistemo-logical obstacle in our understanding of the quantum picture of the world.