Search

The increased complexity of modern system designs and demands for quicker time to market have made safety-related verification and validation of such systems more challenging. Incorporating safety and risk considerations at the early stages of design is one way to acquire a more robust initial design for novel systems. Inductive fault analysis has its significance at final stages of design, e.g., verification and validation. However, to preclude certain system failure states—especially for the systems with high failure consequences, a designer would innately prefer to trace back and remedy the causes of failure, as compared to a more cumbersome activity of identifying the faults individually and sifting the combinations that lead to the failure of interest. The work presented in this paper is aimed at the development of a backward failure propagation methodology for analyzing the origins of functional failures in a conceptual design of systems including but not limited to nuclear, mechanical, aerospace, process, electrical/electronics, telecommunication, automotive, etc. This method allows the designer to achieve a robust early design based on the analyses of the system's functional dependencies before proceeding to the detailed design and testing stages. The insights provided by the analysis at the conceptual design stage also reduce redesign efforts, testing costs, and project delays. The proposed method is a functional analysis approach that extends the Integrated System Failure Analysis for backward failure propagation. When provided with an abstract system configuration, a system's functional model, and a system's behavioral model, it utilizes a known functional state (typically a failure) to acquire system component modes and the states of other functions. The method includes inversion of the functional failure logic and component behavioral rules using propositional logic and deductive analysis to assess valid states of a system that satisfy the given initial conditions. To test the method's scalability, we applied the proposed method to a simplified representation of the secondary loop of a typical pressurized water reactor. [ABSTRACT FROM AUTHOR]

Natural language does not express all connectives definable in classical logic as simple lexical items. Coordination in English is expressed by conjunction and, disjunction or, and negated disjunction nor. Other languages pattern similarly. Non-lexicalized connectives are typically expressed compositionally: in English, negated conjunction is typically expressed by combining negation and conjunction (not both). This is surprising: if ∧ and ∨ are duals, and the negation of the latter can be expressed lexically (nor), why not the negation of the former? I present a two-tiered model of the semantics of the binary connectives. The first tier captures the expressive power of the lexicon: it is a bilateral state-based semantics that, under a restriction, can express all and only the distinctions that can be expressed by the lexicon of natural language (and, or, nor). This first tier is characterized by rejection as non-assertion and a Neglect Zero assumption. The second tier is obtained by dropping the Neglect Zero assumption and enforcing a stronger notion of rejection, thereby recovering classical logic and thus definitions for all Boolean connectives. On the two-tiered model, we distinguish the limited expressive resources of the lexicon and the greater combinatorial expressive power of the language as a whole. This gives us a logic-based account of compositionality for the Boolean fragment of the language. [ABSTRACT FROM AUTHOR]

Rhetorical structure theory (RST) and relational propositions have been shown useful in analyzing texts as expressions in propositional logic. Because these expressions are systematically derived, they may be expected to model discursive reasoning as articulated in the text. If this is the case, it would follow that logical operations performed on the expressions would be reflected in the texts. In this paper the logic of relational propositions is used to demonstrate the applicability of transitive inference to discourse. Starting with a selection of RST analyses from the research literature, analyses of the logic of relational propositions are performed to identify their corresponding logical expressions and within each expression to identify the inference path implicit within the text. By eliminating intermediary relational propositions, transitivity is then used to progressively compress the expression. The resulting compressions are applied to the corresponding texts and their compressed RST analyses. The application of transitive inference to logical expressions results in abridged texts that are intuitively coherent and logically compatible with their originals. This indicates an underlying isomorphism between the inferential structure of logical expressions and discursive coherence, and it confirms that these expressions function as logical models of the text. Potential areas for application include knowledge representation, logic and argumentation, and RST validation. [ABSTRACT FROM AUTHOR]

This paper proposes a deletion algorithm for the marginal problem in propositional logic. The algorithm is based on the general Davis and Putnam deletion algorithm DP, expressed as a bucket elimination algorithm, representing sets of clauses with the same set of variables employing a Boolean array. The main contribution is the development of alternative procedures when deleting a variable which allow more efficient computations. In particular, it takes advantage of the case in which the variable to delete is determined by a subset of the rest of the variables. It also provides a set of useful results and tools for reasoning with Boolean tables. The algorithms are implemented using Python and the NumPy library. Experiments show that this procedure is feasible for intermediate problems and for difficult problems from hard Bayesian networks cases [ABSTRACT FROM AUTHOR]

The increasing significance of theorem proving-based formalization in mathematics and computer science highlights the necessity for formalizing foundational mathematical theories. In this work, we employ the Coq interactive theorem prover to methodically formalize the language, semantics, and syntax of propositional logic, a fundamental aspect of mathematical reasoning and proof construction. We construct four Hilbert-style axiom systems and a natural deduction system for propositional logic, and establish their equivalences through meticulous proofs. Moreover, we provide formal proofs for essential meta-theorems in propositional logic, including the Deduction Theorem, Soundness Theorem, Completeness Theorem, and Compactness Theorem. Importantly, we present an exhaustive formal proof of the Completeness Theorem in this paper. To bolster the proof of the Completeness Theorem, we also formalize concepts related to mappings and countability, and deliver a formal proof of the Cantor–Bernstein–Schröder theorem. Additionally, we devise automated Coq tactics explicitly designed for the propositional logic inference system delineated in this study, enabling the automatic verification of all tautologies, all internal theorems, and the majority of syntactic and semantic inferences within the system. This research contributes a versatile and reusable Coq library for propositional logic, presenting a solid foundation for numerous applications in mathematics, such as the accurate expression and verification of properties in software programs and digital circuits. This work holds particular importance in the domains of mathematical formalization, verification of software and hardware security, and in enhancing comprehension of the principles of logical reasoning. [ABSTRACT FROM AUTHOR]

Definition: In deep learning, large language models are typically trained on data from a corpus as representative of current knowledge. However, natural language is not an ideal form for the reliable communication of concepts. Instead, formal logical statements are preferable since they are subject to verifiability, reliability, and applicability. Another reason for this preference is that natural language is not designed for an efficient and reliable flow of information and knowledge, but is instead designed as an evolutionary adaptation as formed from a prior set of natural constraints. As a formally structured language, logical statements are also more interpretable. They may be informally constructed in the form of a natural language statement, but a formalized logical statement is expected to follow a stricter set of rules, such as with the use of symbols for representing the logic-based operators that connect multiple simple statements and form verifiable propositions. [ABSTRACT FROM AUTHOR]

The study of coherent association rules based on propositional logic is an important area of association rule mining. Users may get a large number of itemsets for low minsup and lose valuable itemsets for high minsup. Mining without minsup may cause itemset explosions that contain spurious itemsets with low correlations and take a long time to mine. For mining coherence rules, existing approaches consider only the frequent itemsets, ignoring rare itemsets. Moreover, all items in the database are regarded equally important, which is not practical in real-world applications. By using the confidence-lift specified multiple minimum supports combined with propositional logic, we propose an efficient approach called rare correlated coherent association rule mining that addresses all of the problems stated above. We define and incorporate termination bound of support (⁠|${s}_{TB}$|⁠) and termination bound of dissociation (⁠|${d}_{TB}$|⁠) for early pruning of the candidate itemsets. In the proposed approach, support thresholds are automatically applied to the itemsets and coherent association rules are derived from the frequent and rare itemsets with high correlation and confidence. Experimental results obtained from real-life datasets show the effectiveness of the proposed approach in terms of itemsets and rule generation, correlation, confidence, runtime and scalability. [ABSTRACT FROM AUTHOR]

Developing a suggestion of Wittgenstein, I provide an account of truth tables as formulas of a formal language. I define the syntax and semantics of TPL (the language of Tabular Propositional Logic) and develop its proof theory. Single formulas of TPL, and finite groups of formulas with the same top row and TF matrix (depiction of possible valuations), are able to serve as their own proofs with respect to metalogical properties of interest. The situation is different, however, for groups of formulas whose top rows differ. [ABSTRACT FROM AUTHOR]

The Tsetlin Machine (TM) is a recent machine learning algorithm with several distinct properties, such as interpretability, simplicity, and hardware-friendliness. Although numerous empirical evaluations report on its performance, the mathematical analysis of its convergence is still open. In this article, we analyze the convergence of the TM with only one clause involved for classification. More specifically, we examine two basic logical operators, namely, the “IDENTITY”- and “NOT” operators. Our analysis reveals that the TM, with just one clause, can converge correctly to the intended logical operator, learning from training data over an infinite time horizon. Besides, it can capture arbitrarily rare patterns and select the most accurate one when two candidate patterns are incompatible, by configuring a granularity parameter. The analysis of the convergence of the two basic operators lays the foundation for analyzing other logical operators. These analyses altogether, from a mathematical perspective, provide new insights on why TMs have obtained state-of-the-art performance on several pattern recognition problems. [ABSTRACT FROM AUTHOR]

This paper presents the multi-adjoint lattice logic (MLL) and its completeness and soundness. Specifically, the proposed many-valued propositional logic framework is defined on a multi-adjoint algebra whose underlying algebraic structure is a bounded lattice, which embeds the well-known basic logic (BL) given by Hájek on residuated lattices. The consideration of truth-stressing hedges in the multi-adjoint algebra is also studied and, as a consequence, two new logics extensions of MLL arise: the multi-adjoint lattice logic very true intensified (MLL v t) and the multi-adjoint lattice logic ∨-very true intensified (MLL ∨ − v t). Finally, the soundness and completeness of the aforementioned logics are also proven. [ABSTRACT FROM AUTHOR]

The class UMU consists of propositional formulas which are a union of minimal unsatisfiable formulas (MU formulas). The structural complexity of UMU formulas depends essentially on the type and degree of intertwining of the MU subformulas. Starting from class of formulas that consist only of clause (or variable) disjoint minimal unsatisfiable subformulas, we study various UMU subclasses given by weakening and these conditions. Generalizing an idea from [6] , we investigate a characterization of UMU formulas by whether they allow transformation into a MU formula by adding literals and/or clauses. It can be shown that simplicity in constructing of such extensions correlates with the degree of intertwining of the MU subformulas. For UMU formulas, however, we can give only extensions that have an exponential size in the worst case. The question of the existence of short MU combinations of MU-formulas by adding literals and clauses remains open. [ABSTRACT FROM AUTHOR]

When people seek to understand concepts from an incomplete set of examples and counterexamples, there is usually an exponentially large number of classification rules that can correctly classify the observed data, depending on which features of the examples are used to construct these rules. A mechanistic approximation of human concept-learning should help to explain how humans prefer some rules over others when there are many that can be used to correctly classify the observed data. Here, we exploit the tools of propositional logic to develop an experimental framework that controls the minimal rules that are simultaneously consistent with the presented examples. For example, our framework allows us to present participants with concepts consistent with a disjunction and also with a conjunction, depending on which features are used to build the rule. Similarly, it allows us to present concepts that are simultaneously consistent with two or more rules of different complexity and using different features. Importantly, our framework fully controls which minimal rules compete to explain the examples and is able to recover the features used by the participant to build the classification rule, without relying on supplementary attention-tracking mechanisms (e.g. eye-tracking). We exploit our framework in an experiment with a sequence of such competitive trials, illustrating the emergence of various transfer effects that bias participants' prior attention to specific sets of features during learning. [ABSTRACT FROM AUTHOR]

Minimizing the cost function that corresponds to propositional logic is vital to ensure the learning phase of HNN can occur optimally. In that regard, optimal and non-biased algorithm is required to ensure HNN will always converge to global solution. Ant Colony Optimization (ACO) is a population-based and nature-inspired algorithm to solve various combinatorial optimization problems. ACO simulates the behaviour of the real ants that forage for food and communication of ants through pheromone density. In this work, ACO will be used to minimize the cost function that corresponds to the logical rule in Hopfield Neural Network. ACO will utilize pheromone density to find the optimal path that leads to zero cost function without consuming more learning iteration. Performance for all learning models will be evaluated based on various performance metrics. Results collected from computer simulation implies that ACO outperformed conventional learning model in minimizing the logical cost function. [ABSTRACT FROM AUTHOR]

Knowledge compilation is an alternative solution to address demanding reasoning tasks with high complexity via converting knowledge bases into a suitable target language. The notion of logical separability, proposed by Levesque, offers a general explanation for the tractability of clausal entailment for two remarkable languages: decomposable negation normal form and prime implicates. It is interesting to explore what role logical separability plays in problem tractability. In this paper, we apply the notion of logical separability to a number of reasoning problems within the context of propositional logic: satisfiability checking (CO), clausal entailment checking (CE), model counting (CT), model enumeration (ME) and forgetting (FO), as well as their dual tasks, contributing to several recursive procedures. We provide the corresponding logical separability based properties: CO-logical separability, CE-logical separability, CT-logical separability, ME-logical separability and their duals. Based on these properties, we then identify four novel normal forms: CO - LSNNF , CE - LSNNF , CT - LSNNF and ME - LSNNF , as well as their dual languages. We show that each of them is the necessary and sufficient condition under which the corresponding procedure is correct. We finally integrate the above normal forms into the knowledge compilation map. [ABSTRACT FROM AUTHOR]

This paper introduces a logical characterization of multi-adjoint algebras with a twofold contribution. On the one hand, the study of multi-adjoint algebras, from a logical perspective, will allow us to discover both the core and new features of these algebras. On the other hand, the axiomatization of multi-adjoint algebras will be useful to take advantage of the properties of the logical connectives considered in the corresponding deductive system. The mechanism considered to carry out the mentioned axiomatization follows the one given by Petr Hájek for residuated lattices. Specifically, the paper presents the bounded poset logic (BPL) as an axiomatization of a bounded poset, since this algebraic structure is the most simple structure from which a multi-adjoint algebra is defined. In the following, the language of BPL is enriched with a family of pairs, composed of a conjunctor and an implication, and its axiomatic system is endowed with new axioms, giving rise to the multi-adjoint logic (ML). The soundness and completeness of BPL and ML are proven. Finally, a comparison between the axiomatization of the multi-adjoint logic and the one given for the BL logic is introduced. [ABSTRACT FROM AUTHOR]

Basic results of the paper are that any four-valued expansion L4 of Dunn-Belnap's logic DB4 is defined by a unique (up to isomorphism) conjunctive matrix M4 with exactly two distinguished values over an expansion U4 of a De Morgan non-Boolean four-valued diamond, but by no matrix with either less than four values or a single [non-]distinguished value, and has no proper extension satisfying Variable Sharing Property (VSP). We then characterize L4's having a theorem / inconsistent formula, satisfying VSP and being [inferentially] maximal / subclassical / maximally paraconsistent, in particular, algebraically through M4jA4's (not) having certain submatricesjsubalgebras. Likewise, [providing U4 is regular / has no three-element subalgebra] L4 has a proper consistent axiomatic extension if[f]M4 has a proper paraconsistent / two-valued submatrix [in which case the logic of this submatrix is the only proper consistent axiomatic extension of L4 and is relatively axiomatized by the Excluded Middle law axiom]. As a generic tool (applicable, in particular, to both classically-negative and implicative expansions of DB4), we also prove that the lattice of axiomatic extensions of the logic of an implicative matrixMwith equality determinant is dual to the distributive lattice of lower cones of the set of all submatrices of M with non-distinguished values. [ABSTRACT FROM AUTHOR]

A propositional logic sentence in conjunctive normal form that has clauses of length at most two (a 2-CNF) can be associated with a multigraph in which the vertices correspond to the variables and edges to clauses. We show that every 2-CNF that has been reduced under the application of certain tautologies, is equisatisfiable to a 2-CNF whose associated multigraph is, in fact, a simple graph. Our main result is a complete characterization of graphs that can support unsatisfiable 2-CNF sentences. We show that a simple graph can support an unsatisfiable reduced 2-CNF sentence if and only if it contains any one of four specific small graphs as a topological minor. Equivalently, all reduced 2-CNF sentences supported on a given simple graph are satisfiable if and only if all subdivisions of those four graphs are forbidden as subgraphs of the original graph. [ABSTRACT FROM AUTHOR]

First-order formalisations are often preferred to propositional ones because they are thought to underwrite the validity of more arguments. We compare and contrast the ability of some well-known logics—these two in particular—to formally capture valid and invalid arguments. We show that there is a precise and important sense in which first-order logic does not improve on propositional logic in this respect. We also prove some generalisations and related results of philosophical interest. The rest of the article investigates the results' philosophical significance. A first moral is that the correct way to state the oft-cited superiority of first-order logic vis- à -vis propositional logic is more nuanced than often thought. The second moral concerns semantic theory; the third logic's use as a tool for discovery. A fourth and final moral is that second-order logic's transcendence of first-order logic is greater than first-order logic's transcendence of propositional logic. [ABSTRACT FROM AUTHOR]

Abstract algebraic logic is a theory that provides general tools for the algebraic study of arbitrary propositional logics. According to this theory, every logic L is associated with a matrix semantics Mod*L. This article is a contribution to the systematic study of the so-called truth sets of the matrices in Mod*L. In particular, we show that the fact that the truth sets of Mod*L can be defined by means of equations with universally quantified parameters is captured by an order-theoretic property of the Leibniz operator restricted to deductive filters of L This result was previously known for equational definability without parameters. Similarly, it was known that the truth sets of Mod*L are implicitly definable if and only if the Leibniz operator is injective on deductive filters of L over every algebra. However, it was an open problem whether the injectivity of the Leibniz operator transfers from the theories of L to its deductive filters over arbitrary algebras. We show that this is the case for logics expressed in a countable language, and that it need not be true in general. Finally we consider an intermediate condition on the truth sets in Mod*L that corresponds to the order-reflection of the Leibniz operator. [ABSTRACT FROM AUTHOR]

For each truth-functionally complete set of connectives, we construct a sound and complete natural deduction system containing no axioms and the smallest possible number of inference rules, namely one. [ABSTRACT FROM AUTHOR]

Coalition formation is studied in a setting where agents take part to a group decision-making scenario and where their preferences are expressed via weighted propositional logic, in particular by considering formulas consisting of conjunctions of literals only. Interactions among agents are constrained by an underlying social environment and each agent is associated with a specific social factor determining to which extent she prefers staying in a coalition with other agents. In particular, the utilities of the agents depend not only on their absolute preferences but also on the number of "neighbors" occurring with them in the coalition that emerged. Within this setting, the computational complexity of a number of relevant reasoning tasks is studied, by charting a clear picture of the intrinsic difficulty of finding "agreements" among the agents. Specific algorithmic approaches to reason about such social environments are proposed under the utilitarian perspective, where the collective utility of a coalition is the sum of the utilities of the individuals, as well as under the egalitarian perspective, with the goal being to maximize the utility of the least satisfied agent. These algorithms have been implemented and results of experimental activity are discussed, too. [ABSTRACT FROM AUTHOR]

Boolean games allow us to succinctly represent strategic games with binary payoffs in the case where the players' preferences have a structure readily expressible in propositional logic. Since their introduction, the computational aspects of Boolean games have been of interest to the multiagent community, but so far the focus has been exclusively on pure strategy equilibria. In this paper we consider the complexity of problems involving mixed strategy equilibria, such as the existence of an equilibrium satisfying a given payoff constraint. The results are obtained by the observation that a mixed strategy can hold enough information to encode the computation history of an exponential time Turing machine. [ABSTRACT FROM AUTHOR]

The overall purpose of the present work is to lay the foundations for a new approach to bridge logic and probabilistic computation. To this aim we introduce extensions of classical and intuitionistic propositional logic with counting quantifiers , that is, quantifiers that measure to which extent a formula is true. The resulting systems, called cCPL and iCPL , respectively, admit a natural semantics, based on the Borel σ -algebra of the Cantor space, together with a sound and complete proof system. Our main results consist in relating cCPL and iCPL with some central concepts in the study of probabilistic computation. On the one hand, the validity of cCPL -formulae in prenex form characterizes the corresponding level of Wagner's hierarchy of counting complexity classes, closely related to probabilistic complexity. On the other hand, proofs in iCPL correspond, in the sense of Curry and Howard, to typing derivations for a randomized extension of the λ -calculus, so that counting quantifiers reveal the probability of termination of the underlying probabilistic programs. [ABSTRACT FROM AUTHOR]

Belief merging aims to combine pieces of information from different (and possibly conflicting) sources so as to produce a single consistent belief base which retains as much information as possible. In this paper, we describe Merginator, a logic-based tool implementing three belief merging operators presented with specific characteristics that make them interesting for comparison: ΔΣ, ΔGMax and Δps. We describe these operators while solving a set of basic examples found in the literature that we translate into natural language to provide insights for Merginator users. We also propose two more complex consensus-seeking examples: an adaptation to the role play “Lost at Sea” and the subject of administrative response to air pollution in Hong Kong. Results show that all three operators provide a consensus to the scenarios, and Δps gives the most refined consensus. This demonstrates that belief merging, is a viable technique to support consensus decision-making in many domains. Merginator is open source software available at GitHub. [ABSTRACT FROM AUTHOR]

Purpose The starting point of this paper is the propositional model of conflict resolution which was presented and critically discussed in Lempp (2016). Based on this model, a software implementation, called ProCON, is introduced and applied to three scenarios. The purpose of the paper is to demonstrate how ProCON can be used by negotiators and to evaluate ProCON’s practical usefulness as an automated negotiation support system.Design/methodology/approach The propositional model is implemented as a computer program. The implementation consists of an input module to enter data about a negotiation situation, an output module to generate outputs (e.g. a list of all incompatible goal pairs or a graph displaying the compatibility relations between goals) and a queries module to run queries on particular aspects of a negotiation situation.Findings The author demonstrates how ProCON can be used to capture a simple two-party, non-iterative prisoner’s dilemma, applies ProCON to a contract negotiation between a supplier and a purchaser of goods, and uses it to model the negotiations between the Iranian and six Western governments over Iran’s nuclear enrichment and stockpiling capacities.Research limitations/implications A limitation of the current version of ProCON arises from the fact that the computational complexity of the underlying algorithm is EXPTIME (i.e. the computing time required to process information in ProCON grows exponentially with respect to the number of issues fed into the program). This means that computing time can be quite long for even relatively small negotiation scenarios.Practical implications The three case studies demonstrate how ProCON can provide support for negotiators in a wide range of multi-party, multi-issue negotiations. In particular, ProCON can be used to visualise the compatibility relations between parties’ goals, generate possible outcomes and solutions and evaluate solutions regarding the extent to which they satisfy the parties’ goals.Originality/value In contrast to standard game-theoretic models of negotiation, ProCON does not require users to provide data about their preferences across their goals. Consequently, it can operate in situations where no information about the parties’ goal preferences is available. Compared to game-theoretical models, ProCON represents a more general approach of looking at possible outcomes in the context of negotiations. [ABSTRACT FROM AUTHOR]

Jan Dullaert (1480-1513) was a direct student of John Mair and a teacher of Gaspar Lax, Juan de Celaya, and Juan Luis Vives. His commentary on Aristotle's Peri Hermeneias addresses the foundations of propositional logic, including a detailed analysis of conditionals (following Paul of Venice's Logica magna) and the semantics of logical connectives (conjunction, disjunction, and implication). Dullaert's propositional logic is limited to the immediate implications of the semantics of these connectives, i.e., their introduction and elimination rules. In the same context, he discusses several alternative treatments of semantic paradoxes, paying most attention to the approaches derived from Martin Le Maistre (based on the idea that sentential meaning is closed under entailment) and John Mair (based on the idea that self-falsifying sentences are false). [ABSTRACT FROM AUTHOR]

This study offers an analysis of independent conditional clauses (ICCs) that are used with argumentative functions in spoken Dutch. ICCs are used as arguments when they serve to motivate the speaker's implied standpoint regarding a preceding propositional content, termed the trigger. Two basic types of argumentative ICCs can be distinguished, which are termed "direct" and "indirect" arguments. Direct arguments express a contextually given premise on the basis of which a conclusion about the speaker's standpoint regarding a preceding trigger can be drawn. Indirect arguments, by contrast, express a condition that - if it had held - would have warranted the conclusion, but its counterfactual interpretation resulting from hypothetical backshift signals that the speaker knows that this condition is not fulfilled, and hence that the implied standpoint regarding a trigger is not valid either. We argue that direct and indirect ICCs instantiate independent instances of epistemic non-predictive conditionals and hypothetical predictive conditionals (in the sense of Dancygier), respectively, and that they set up propositional-logic arguments of different classic forms, i.e. the modus ponendo ponens form (direct ICCs) and the denying the antecedent form (indirect ICCs). However, they do not explicitly express the conclusion of the argument, as they lack a main clause, but leave it to be inferred by the addressee. [ABSTRACT FROM AUTHOR]

The paper continues the line of [6–8] . This results in a model-theoretic characterization of expressive powers of arbitrary finite sets of guarded connectives of degree not exceeding 1 and regular connectives of degree 2 over the language of bounded lattices. [ABSTRACT FROM AUTHOR]

Redundancy checking (RC) is a key knowledge reduction technology. Extension rule (ER) is a new reasoning method, first presented in 2003 and well received by experts at home and abroad. Novel extension rule (NER) is an improved ER-based reasoning method, presented in 2009. In this paper, we first analyse the characteristics of the extension rule, and then present a simple algorithm for redundancy checking based on extension rule (RCER). In addition, we introduce MIMF, a type of heuristic strategy. Using the aforementioned rule and strategy, we design and implement RCHER algorithm, which relies on MIMF. Next we design and implement an RCNER (redundancy checking based on NER) algorithm based on NER. Parallel computing greatly accelerates the NER algorithm, which has weak dependence among tasks when executed. Considering this, we present PNER (parallel NER) and apply it to redundancy checking and necessity checking. Furthermore, we design and implement the RCPNER (redundancy checking based on PNER) and NCPPNER (necessary clause partition based on PNER) algorithms as well. The experimental results show that MIMF significantly influences the acceleration of algorithm RCER in formulae on a large scale and high redundancy. Comparing PNER with NER and RCPNER with RCNER, the average speedup can reach up to the number of task decompositions when executed. Comparing NCPNER with the RCNER-based algorithm on separating redundant formulae, speedup increases steadily as the scale of the formulae is incrementing. Finally, we describe the challenges that the extension rule will be faced with and suggest possible solutions. [ABSTRACT FROM AUTHOR]

In artificial intelligence, it is important to handle and analyse inconsistency in knowledge bases. Inconsistent pieces of information suggest questions like “where is the inconsistency?” and “how severe is it?”. Inconsistency measures have been proposed to tackle the latter issue, but the former seems underdeveloped and is the focus of this paper. Minimal inconsistent sets have been the main tool to localise inconsistency, but we argue that they are like the exposed part of an iceberg, failing to capture contradictions hidden under the water. Using classical propositional logic, we develop methods to characterise when a formula is contributing to the inconsistency in a knowledge base and when a set of formulas can be regarded as a primitive conflict. To achieve this, we employ an abstract consequence operation to “look beneath the water level”, generalising the minimal inconsistent set concept and the related free formula notion. We apply the framework presented to the problem of measuring inconsistency in knowledge bases, putting forward relaxed forms for two debatable postulates for inconsistency measures. Finally, we discuss the computational complexity issues related to the introduced concepts. [ABSTRACT FROM AUTHOR]

This paper studies Cellular Automata with binary states on monoids making use of formulae in propositional logic, instead of local functions. Also we prove that the multiplication of formulae, defined by monoid action, determines the composition of transition functions of CA. This result converts the reversibility of transition functions to the reversibility of formulae. Several examples of reversible formulae are illustrated. Finally, introducing the Stone topology on configuration spaces, we give a neat proof of Hedlund's theorem for CA. [ABSTRACT FROM AUTHOR]

Product configuration is when an artifact from a product family is assembled from a set of predefined components that can only be combined in certain ways. These ways are defined by configuration rules. The product developers inspect the configuration rules when they develop new configuration rules or modify the configuration rules set. The inspection of configuration rules is thereby an important activity to avoid errors in the configuration rules set. Several formulations of constraint satisfaction problems (CSPs) are proposed that facilitate the inspection of configuration rules in propositional logic (IF-THEN, AND, NOT, OR, etc.). Many of the configuration rules are so called production rules; that is, a configuration rule is an IF-THEN expression that fires when the IF condition is met. Several configuration rules build chains that fire during the product configuration. It is therefore important not only to inspect single configuration rules but also to analyze the effect of multiple configuration rules. Formulating the tasks as variations of the CSP can support the inspection activity. More specifically, we address the reformulation of configuration rules, testing of feature variant combinations, and counting of item quantities from an item set. The suggested CSPs are tested on industrial vehicle configuration rules for computational performance. The results show that the time for achieving results from the solving of the CSP is within seconds. Our future work will be to implement the various CSPs into a demonstrator that could be tested by product developers. [ABSTRACT FROM AUTHOR]

Purpose – The purpose of this paper is to explore the extent to which formal logic can be applied to conflict analysis and resolution. It is motivated by the idea that conflicts can be understood as inconsistent sets of interests. Design/methodology/approach – A simple propositional model, based on propositional logic, which can be used to analyze conflicts, has been introduced and four algorithms have been presented to generate possible solutions to a conflict. The model is illustrated by applying it to the conflict between the Obama administration and the Syrian Government in September 2013 over the destruction of Syria’s chemical weapons programme. Findings – The author shows how different solutions, such as compromises, minimally invasive solutions or solutions compatible with certain pre-defined norms, can be generated by the model. It is shown how the model can operate in situations where the game-theoretic model fails due to a lack of information about the parties’ utility values. Research limitations/implications – The model can be used as a theoretical framework for future experimental research and/or to trace the course of particular conflict scenarios. Practical implications – The model can be used as the basis for building software applications for conflict resolution practitioners, such as negotiators or mediators. Originality/value – While the idea of using logic to analyse the structure of conflicts and generate possible solutions is not new to the field of conflict studies, the model presented in this paper provides a novel way of understanding conflicts for both researchers and practitioners. [ABSTRACT FROM AUTHOR]

In this paper we consider an extended variant of query learning where the hidden concept is embedded in some Boolean circuit. This additional processing layer modifies query arguments and answers by fixed transformation functions which are known to the learner. For this scenario, we provide a characterization of the solution space and an ordering on it. We give a compact representation of the minimal and maximal solutions as quantified Boolean formulas and we adapt the original algorithms for exact learning of specific classes of propositional formulas. [ABSTRACT FROM AUTHOR]

A propositional logic induced by means of commutative basic algebras was already described by M. Botur and R. Halaš. It turns out that this is a kind of non-associative fuzzy logic which can be used e.g. in expert systems. Unfortunately, there are other important classes of basic algebras which are not commutative, e.g. orthomodular lattices which are used as an axiomatization of the logic of quantum mechanics. This motivated us to develop another axioms and derivation rules which form a propositional logic induced by basic algebras in general. We show that this logic is algebraizable in the sense of W. J. Blok and D. Pigozzi. [ABSTRACT FROM AUTHOR]

The aim of the paper is to introduce and describe tense operators in every propositional logic which is axiomatized by means of an algebra whose underlying structure is a bounded poset or even a lattice. We introduce the operators G, H, P and F without regard what propositional connectives the logic includes. For this we use the axiomatization of universal quantifiers as a starting point and we modify these axioms for our reasons. At first, we show that the operators can be recognized as modal operators and we study the pairs ( P, G) as the so-called dynamic order pairs. Further, we get constructions of these operators in the corresponding algebra provided a time frame is given. Moreover, we solve the problem of finding a time frame in the case when the tense operators are given. In particular, any tense algebra is representable in its Dedekind-MacNeille completion. Our approach is fully general, we do not relay on the logic under consideration and hence it is applicable in all the up to now known cases. [ABSTRACT FROM AUTHOR]

Conditional independence provides an essential framework to deal with knowledge and uncertainty in Artificial Intelligence, and is fundamental in probability and multivariate statistics. Its associated implication problem is paramount for building Bayesian networks. Unfortunately, the problem does not enjoy an axiomatization, by a finite set of Horn rules, and is already coNP-complete to decide for some fragments of conditional independencies. Saturated conditional independencies form an important fragment whose implication problem is decidable in almost linear time. We establish an axiomatization, by a finite set of Horn rules, for the fragment of generalized saturated conditional independencies. These state the conditional independence between finitely many sets of random variables. The special case of two sets captures Geiger and Pearl's finite axiomatization for saturated conditional independencies. Even for this special case, our completeness proof is new. The proof argument utilizes special probability models where two events have probability one half. Special probability models allow us to establish an equivalence between the implication of generalized saturated conditional independencies and that of formulae in a Boolean propositional fragment. This duality is then extended to a trinity including the implication problem of Delobel's full first-order hierarchical database decompositions. Already for the independence between two sets of random variables, the dualities cannot be extended to cover conditional independencies in general, or first-order hierarchical decompositions. [ABSTRACT FROM AUTHOR]

Analogues of the classical omitting types theorems of frst-order logic are proved for propositional logic. For an infnite cardinal κ, a suficient criterion is given for the omission of κ-many types in a propositional language with κ propositional variables. [ABSTRACT FROM AUTHOR]

In this paper, we study Reiter's propositional default logic when the treewidth of a certain graph representation (semi-primal graph) of the input theory is bounded. We establish a dynamic programming algorithm on tree decompositions that decides whether a theory has a consistent stable extension (Cons). Our algorithm can even be used to enumerate all generating defaults (EnumSD) that lead to stable extensions. We show that our algorithm decides Cons in linear time in the input theory and triple exponential time in the treewidth Further, our algorithm solves EnumSD with a pre-computation step that is linear in the input theory and triple exponential in the treewidth followed by a linear delay to output solutions. Finally, we take the exponential time hypothesis (ETH) into consideration and establish lower bounds of bounded treewidth algorithms for Cons. [ABSTRACT FROM AUTHOR]