This is the first publication on complete and stand alone arithmetization of bivalent logic.

The Joint International Conference on Logic Programming, sponsored by the Association for Logic Programming, is a major forum for presentations of research, applications, and implementations in this important area of computer science. Logic programming is one of the most promising steps toward declarative programming and forms the theoretical basis of the programming language Prolog and its various extensions. Logic programming is also fundamental to work in artificial intelligence, where it has been used for nonmonotonic and commonsense reasoning, expert systems (...) implementation, deductive databases, and applications such as computer-aided manufacturing. Krzysztof R. Apt is project leader at the Centre for Mathematics and Computer Science in Amsterdam and part-time Professor in Computer Science at the University of Amsterdam. Topics covered: Theory Foundations. Programming Languages. Implementation. Programming Methodologies and Tools. Applications. Deductive Databases. Artificial Intelligence. Parallelism. (shrink)

The truth of every human being is the end his life with death, and this leads to leaving assets and funds for those after him and can lead to hate between the heirs, it has made a point of Islamic law on all aspects of life, including the subject of the inheritance of the deceased. The main problem is how to get the knowledge of the basics of inheritance. This paper reviews work done in the use of expert (...) class='Hi'>system software to calculate inheritance in Islam. A proposed expert system was designed and developed using CLIPS language to calculate the inheritance in Islam. (shrink)

Background: Depression (major depressive disorder) is a common and serious medical illness that negatively affects how you feel, the way you think and how you act. Fortunately, it is also treatable. Depression causes feelings of sadness and/or a loss of interest in activities once enjoyed. It can lead to a variety of emotional and physical problems and can decrease a person’s ability to function at work and at home. Depression affects an estimated one in 15 adults (6.7%) in any given (...) year. And one in six people (16.6%) will experience depression at some time in their life. Depression can strike at any time, but on average, first appears during the late teens to mid-20s. Women are more likely than men to experience depression. Some studies show that one-third of women will experience a major depressive episode in their lifetime. Objectives: The main goal of this expert system is to get the appropriate diagnosis of disease and the correct treatment and give the appropriate method of treatment through several tips that concern the disease and how to treat it and we will see it through the application on the expert system. Methods: in this paper the design of the proposed Expert System which was produced to help Psychologist in diagnosing depression disease through its symptoms such as: a loss of energy, a change in appetite, sleeping more or less, anxiety, reduced concentration, indecisiveness, restlessness, feelings of worthlessness, guilt or hopelessness and thoughts of self-harm or suicide. The proposed expert system presents an overview about depression disease is given, the cause of diseases is outlined and the treatment of disease whenever possible is given out. SL5 Object Expert System language was used for designing and implementing the proposed expert system. Results: The proposed depression disease diagnosis expert system was evaluated by psychologist students and they were satisfied with its performance. Conclusions: The Proposed expert system is very useful for psychologist, patients with depression and newly graduated psychologist. (shrink)

The paper seeks to identify how teacher expertise is implicitly and explicitly conceptualised in current English education policy in respect of the professional development of teachers. We focus specifically on conceptualisations of expertise in the Early Career Framework (ECF), both in terms of the policy documentation produced by the Department for Education and in terms of a selection of publicly available materials produced by the lead providers of the ECF. We aim to locate these conceptualisations in terms of broader sociological (...) and philosophical debates about the nature of expertise and its relationship to professional work, in addition to recent research on the policy context of teacher education and professional development in England. Our analysis reveals the inappropriacy of ‘expert systems’ approaches to expertise in educational contexts, the underlying assumptions embedded in policy in terms of what constitutes high-quality teaching practice and the insufficiency of relying on an appointed advisory group and organisations preferred by government for identifying and iterating criteria for expertise. (shrink)

Background: Arthritis is very common but is not well understood. Actually, “arthritis” is not a single disease; it is an informal way of referring to joint pain or joint disease. There are more than 100 different types of arthritis and related conditions. People of all ages, sexes and races can and do have arthritis, and it is the leading cause of disability in America. More than 50 million adults and 300,000 children have some type of arthritis. It is most common (...) among women and occurs more frequently as people get older. Common arthritis joint symptoms include swelling, pain, stiffness and decreased range of motion. Symptoms may come and go. They can be mild, moderate or severe. They may stay about the same for years, but may progress or get worse over time. Severe arthritis can result in chronic pain, inability to do daily activities and make it difficult to walk or climb stairs. Arthritis can cause permanent joint changes. These changes may be visible, such as knobby finger joints, but often the damage can only be seen on X-ray. Some types of arthritis also affect the heart, eyes, lungs, kidneys and skin as well as the joints. Objectives: The main goal of this expert system is to get the appropriate diagnosis of disease and the correct treatment and give the appropriate method of treatment through several tips that concern the disease and how to treat it and we will see it through the application on the expert system. Methods: in this paper the design of the proposed Expert System which was produced to help Orthopedist in diagnosing Arthritis disease through its symptoms such as: pain on pressure in a joint , Inflammation indicated by joint swelling, Stiffness especially in the morning , Loss of flexibility of joint, Limited, joint movement, Deformity of the joints , Weight loss and fatigue , Non-specific fever and Crepitus. The proposed expert system presents an overview about Arthritis disease is given, the cause of diseases is outlined and the treatment of disease whenever possible is given out. SL5 Object Expert System language was used for designing and implementing the proposed expert system. Results: The proposed Arthritis disease diagnosis expert system was evaluated by Orthopedics students and they were satisfied with its performance. Conclusions: The Proposed expert system is very useful for Orthopedist, patients with arthritis and newly graduated Orthopedics students. (shrink)

Expert systems provide new languages and a new methodology for automating knowledge-intensive processes. Whilst the benefits expected are ubiquitously stated, probable negative impacts are seldom admitted by the dominant actors in the field. We deal with probable problematic impacts on employment as well as contents and structure of work both in production and the service and administration areas and make some suggestions concerning measures to be taken to account for these impacts assuming no radical change as to the prevailing (...) ideology of working organization. (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)

By studying several cases of expert systems' use, a variety of difficulties were identified as directly depending on specific characteristics of experts and their tasks. This concerns more than the questions: “May experts be replaced by machines?” or “Is experts' knowledge explicable?”. The organisational structure of their work as well as the cyclic, non-plannable way of their task performing have further relevance. The paper introduces the concept of experts' systems to deal with diversities of their expertise and complexities of (...) their work. It draws a distinction between non-monotonic problem solving, exploration, medium and modification, and argues that these modes are not reducible to yet another improved input/output strategy or dialogue style but introduce additional functions supporting the human-computer interaction according to experts' needs. In the first few sections, the paper covers the theoretical and empirical results of our research, whereas Section 4 introduces our design suggestions for experts' systems. (shrink)

Our goal is to develop a syntactical apparatus for propositional logics in which the accepted and rejected propositions have the same status and obeying treated in the same way. The suggested approach is based on the ideas of Łukasiewicz used for the classical logic and in addition, it includes the use of multiple conclusion rules. More precisely, a consequence relation is defined on a set of statements of forms “proposition _A_ is accepted” and “proposition _A_ is rejected”, where _A_ is (...) a proposition,—a unified consequence relation. Accordingly, the rules defining a unified consequence relation,—the unified rules, have statements as premises and as conclusions. A special attention is paid to the logics in which each proposition is either accepted or rejected. If we express this property via unified rules and add them to a unified deductive system, such a unified deductive system defines a reversible unified consequence: a statement “proposition _B_ is accepted” is derived from the statement “proposition _A_ is accepted” if and only if a statement “proposition _A_ is rejected” is derived from the statement “proposition _B_ is rejected”. (shrink)

The relation between logic and thought has long been controversial, but has recently influenced theorizing about the nature of mental processes in cognitive science. One prominent tradition argues that to explain the systematicity of thought we must posit syntactically structured representations inside the cognitive system which can be operated upon by structure sensitive rules similar to those employed in systems of natural deduction. I have argued elsewhere that the systematicity of human thought might better be explained as resulting (...) from the fact that we have learned natural languages which are themselves syntactically structured. According to this view, symbols of natural language are external to the cognitive processing system and what the cognitive system must learn to do is produce and comprehend such symbols. In this paper I pursue that idea by arguing that ability in natural deduction itself may rely on pattern recognition abilities that enable us to operate on external symbols rather than encodings of rules that might be applied to internal representations. To support this suggestion, I present a series of experiments with connectionist networks that have been trained to construct simple natural deductions in sentential logic. These networks not only succeed in reconstructing the derivations on which they have been trained, but in constructing new derivations that are only similar to the ones on which they have been trained. (shrink)

The distinction between the syntactic and the semantic approach to scientific theories emerged in formal philosophy of science. The semantic approach is commonly considered more advanced and more successful than the syntactic one, but the transition from the one approach to the other was not brought about without any loss. In essence, it is the formal analysis of atomic propositions and the analysis of deductive reasoning that dropped out of consideration in at least some of the elaborated versions of the (...) semantic approach. In structuralist theory of science, as founded by Sneed and Stegmüller, the focus is on global propositions concerning the question of whether or not certain empirical systems satisfy a set-theoretic predicate that encodes the axioms of a scientific theory. Hence, an analysis of deductive reasoning from atomic premisses with the help of a given theory is missing. The objective of the present paper is to develop a deductive system on the basis of the structuralist framework. This system comes with a novel formulation of empirical propositions in structuralism. (shrink)

This monograph provides a new account of justified inference as a cognitive process. In contrast to the prevailing tradition in epistemology, the focus is on low-level inferences, i.e., those inferences that we are usually not consciously aware of and that we share with the cat nearby which infers that the bird which she sees picking grains from the dirt, is able to fly. Presumably, such inferences are not generated by explicit logical reasoning, but logical methods can be used to describe (...) and analyze such inferences. Part 1 gives a purely system-theoretic explication of belief and inference. Part 2 adds a reliabilist theory of justification for inference, with a qualitative notion of reliability being employed. Part 3 recalls and extends various systems of deductive and nonmonotonic logic and thereby explains the semantics of absolute and high reliability. In Part 4 it is proven that qualitative neural networks are able to draw justified deductive and nonmonotonic inferences on the basis of distributed representations. This is derived from a soundness/completeness theorem with regard to cognitive semantics of nonmonotonic reasoning. The appendix extends the theory both logically and ontologically, and relates it to A. Goldman's reliability account of justified belief. This text will be of interest to epistemologists and logicians, to all computer scientists who work on nonmonotonic reasoning and neural networks, and to cognitive scientists. (shrink)

Hybrid deduction-refutation systems are presented for four first degree entailment based logics. The hybrid systems are shown to deductively and refutationally sound and complete with respect to their logics. The proofs of completeness are presented in a uniform way. This paper builds on work in [6], where Goranko presented a deductively and refutationally sound and complete hybrid system for classical logic.

On the example of the online game Akinator, the basic principles on which programs of this type are built are considered. Effective technics have been proposed by which artificial intelligence systems can build logical inferences that allow to identify an unknown subject from its description. To confirm the considered hypotheses, the terminological analysis of definition of the program "Akinator" offered by the author is carried out. Starting from the assumptions given by the author's definition, the article complements their definitions presented (...) by other researchers and analyzes their constituent theses. Finally, some proposals are made for the next steps in improving the program. The Akinator program, at one time, became one of the most famous online games using artificial intelligence. And although this was not directly stated, it was clear to the experts in the field of artificial intelligence that the program uses the techniques of expert systems and is built on inference rules. At the moment, expert systems have lost their positions in comparison with the direction of neural networks in the field of artificial intelligence, however, in the case considered in the article, we are talking about techniques using both directions – hybrid systems. Games for filling semantics interact with the user, expanding their semantic base and use certain strategies to achieve the best result. The playful form of such semantics filling programs is beneficial for researchers by involving a large number of players. The article examines the techniques used by the Akinator program, and also suggests possible modifications to it in the future. This study, first of all, focuses on how the knowledge base of the Akinator program is built, it consists of incomplete sets, which can be filled and adjusted as a result of further iterations of the program launches. It is important to note our assumption that the order of questions used by the program during the game plays a key role, because it determines its strategy. It was identified that the program is guided by the principles of nonmonotonic logic – the assumptions constructed by the program are not final and can be rejected by it during the game. The three main approaches to acquisite semantics proposed by Jakub Šimko and Mária Bieliková are considered, namely, expert work, crowdsourcing and machine learning. Paying attention to machine learning, the Akinator program using machine learning to build an effective strategy in the game presents a class of hybrid systems that combine the principles of two main areas in artificial intelligence programs – expert systems and neural networks. (shrink)

This book stands at the intersection of two topics: the decidability and computational complexity of hybrid logics, and the deductive systems designed for them. Hybrid logics are here divided into two groups: standard hybrid logics involving nominals as expressions of a separate sort, and non-standard hybrid logics, which do not involve nominals but whose expressive power matches the expressive power of binder-free standard hybrid logics.The original results of this book are split into two parts. This division reflects the division of (...) the book itself. The first type of results concern model-theoretic and complexity properties of hybrid logics. Since hybrid logics which we call standard are quite well investigated, the efforts focused on hybrid logics referred to as non-standard in this book. Non-standard hybrid logics are understood as modal logics with global counting operators ) whose expressive power matches the expressive power of binder-free standard hybrid logics. The relevant results comprise: 1. Establishing a sound and complete axiomatization for the modal logic K with global counting operators ), which can be easily extended onto other frame classes, 2. Establishing tight complexity bounds, namely NExpTime-completeness for the modal logic with global counting operators defined over the classes of arbitrary, reflexive, symmetric, serial and transitive frames ), MT), MD), MB), MK4) with numerical subscripts coded in binary. Establishing the exponential-size model property for this logic defined over the classes of Euclidean and equivalential frames ), MS5).Results of the second type consist of designing concrete deductive systems for standard and non-standard hybrid logics. More precisely, they include: 1. Devising a prefixed and an internalized tableau calculi which are sound, complete and terminating for a rich class of binder-free standard hybrid logics. An interesting feature of indicated calculi is the nonbranching character of the rule, 2. Devising a prefixed and an internalized tableau calculi which are sound, complete and terminating for non-standard hybrid logics. The internalization technique applied to a tableau calculus for the modal logic with global counting operators is novel in the literature, 3. Devising the first hybrid algorithm involving an inequality solver for modal logics with global counting operators. Transferring the arithmetical part of reasoning to an inequality solver turned out to be sufficient in ensuring termination.The book is directed to philosophers and logicians working with modal and hybrid logics, as well as to computer scientists interested in deductive systems and decision procedures for logics. Extensive fragments of the first part of the book can also serve as an introduction to hybrid logics for wider audience interested in logic.The content of the book is situated in the areas of formal logic and theoretical computer science with some elements of the theory of computational complexity. (shrink)

Varieties of natural deduction systems are introduced for Wansing’s paraconsistent non-commutative substructural logic, called a constructive sequential propositional logic (COSPL), and its fragments. Normalization, strong normalization and Church-Rosser theorems are proved for these systems. These results include some new results on full Lambek logic (FL) and its fragments, because FL is a fragment of COSPL.

A construction principle for natural deduction systems for arbitrary, finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness, and normal-form theorems for natural deduction systems.

George Boole published his account on hypotheticals in his pamphlet The Mathematical Analysis of Logic in 1847. Hypothetical deductions were not as developed as categorical ones by Boole’s time. It was still common practice to reduce hypotheticals to categoricals. Boole innovated by proposing an algebraic method to derive (equations expressing) the conclusions of hypotheticals. He had developed a calculus of classes for categoricals in his first pamphlet chapters and seemingly intended extending it to hypotheticals. Nonetheless, propositions can be only true (...) or false. In contradistinction with his approach for categorical propositions, here it was not possible to consider things or classes of things but only the cases and conjunctures of circumstances in which the propositions are true. Some criticisms have been raised concerning Boole’s view of logic as the solution of algebraic equations. In order to circumvent such criticisms, we construct a deductive system based on Boole's algebraic treatment and apply it to deductions of those hypotheticals analyzed by Boole. We found that Barbara translated in our notation is useful to eliminate symbols in such deductions. The deductive system presented here has the potential to provide a new perspective on Boole’s approach to hypotheticals in The Mathematical Analysis of Logic. (shrink)

The consensus among legal philosophers is probably that rule-based legal expert systems leave much to be desired as aids in legal decision-making. Why? What can we do about it? A bureaucrat administering some set of complex rules will ascertain the facts and apply the rules to them in order to discover their consequences for the case in hand. This process of deductive reasoning is characteristically bureaucratic.

Based on the strict definitions of concepts, such as deduction, the deduction rule and the deduction system, the form axiom, the substantive axiom, this article clearly shows the essence of the deductive reasoning, namely “Related attribute and the related restriction relations, which are conveyed in what the main concept of the deduction refers to, must be contained in those conveyed in what the premise proposition refers to”。Then puts forward the theorem “contradiction can not be derived (...) from the strict deduction system”, and gives the proofs. (shrink)

Three case studies were conducted on the implications of the use of expert systems for the work of clerks and operators in Britain. An expert system had been introduced in a process control application. The operators' work was deskilled. The second case was a fault diagnosis application. An operator was very happy with his new work. In the third case, insurance clerks received training to operate an expert system which extended the scope of their work. (...) In conclusion, it is suggested that expert systems extend the range of work which can be automated, but may not have unique impacts. (shrink)

Often, knowledge engineers become so involved in the development process of the expert system that they fail to look further down the road toward the expert system's institutionalization within the organization. Institutionalization is an important component of the expert system planning process. More specifically, the legal issues associated with expert systems development and deployment are critical institutionalization factors. This paper looks at some expert system institutionalization guidelines, and then focuses on legal (...) considerations. (shrink)

In 1934 Jaśkowski and Gentzen independently published their groundbreaking works on Natural Deduction. The aim of this paper is to provide some criteria for division of the diversity of existing systems on some natural subcategories and to show that despite the differences all these systems are descendants of original systems of Jaśkowski and Gentzen. Three criteria are discussed:The kind of items which are building-blocks of the proof.The format of proof.The kind of rules.The first leads to the division of ND (...) into two main classes: F-systems working on formulas and S-systems working on sequents. The second distinguishes between T-systems with tree-proofs and L-systems with linear proofs. Finally, the third leads to several minor divisions in the main categories. (shrink)

ABSTRACT Real-time graphical interval logic is a modal logic for reasoning about time in which the basic modality is the interval. The logic differs from other logics in that it has a natural intuitive graphical representation that resembles the timing diagrams drawn by system designers. We have developed an automted deduction system for the logic, which includes a theorem prover and a user interface. The theorem prover checks the validity of proofs in the logic and produces counterexamples (...) to invalid proofs. The user interface includes a graphical editor that enables the user to create graphical formulas on a workstation display, and a database and proof manager that tracks proof dependencies and allows graphical formulas to be stored and retrieved. In this paper we describe the logic, the automated deduction system, and an application to robotics. (shrink)

The aim of the paper is to present two natural deduction systems for Intuitionistic Sentential Calculus with Identity ( ISCI ); a syntactically motivated $\mathsf {ND}^1_{\mathsf {ISCI}}$ and a semantically motivated $\mathsf {ND}^2_{\mathsf {ISCI}}$. The formulation of $\mathsf {ND}^1_{\mathsf {ISCI}}$ is based on the axiomatic formulation of ISCI. Its rules cannot be straightforwardly classified as introduction or elimination rules; ISCI -specific rules are based on axioms characterizing the identity connective. The system does not enjoy the standard subformula property, (...) but due to the normalization procedure non-subformulas can label only leaves of proofs. In $\mathsf {ND}^2_{\mathsf {ISCI}}$, we propose only two general identity-related rules, in reference to the treatment of the identity connective in First-Order Logic. (shrink)

In this paper the difficulties arising out of a necessary examination of expert systems as to the ‘correctness’ of functioning are outlined. The argumentation is based on the problematic use of the knowledge term in expert system development and the design perspectives connected with the cognitivistic knowledge concept. It becomes obvious that fundamental problems in system development will involve negative consequences for utilization. The perspective developed from this analysis is assuming that these problems have to be (...) taken into account in development and have to be elucidated for utilization. (shrink)

Today’s everyone normal life can include a normal rate of playing computer games or video games; but what about an excessive or compulsive use of video games that impact on our life? Our kids, who usually spend a lot of time in playing video games will likely have a trouble in paying attention to their school lessons. In this paper, we introduce an expert system to help users in getting the correct diagnosis of the health problem of video (...) game addictions that range from (Musculoskeletal issues, Vision problems and Obesity). Moreover, this expert system provides information about the problem and tell us how we can solve it. SL5 Object expert system language was used to design and implement the expert system. (shrink)

Knowledge representation (KR) is actually more than representation: It involves also inference, namely inference of “new” knowledge, i.e. new facts. Logic programming is a suitable KR medium, but more often than not discussions on this programming paradigm focus on aspects other than KR. In this paper, I elaborate on the general theory of logic programming and give the essentials of two of its main implementations, to wit, Prolog and Datalog, from the viewpoint of deductive computing over knowledge bases, which includes (...) deductive programming. (shrink)

The notion of an algebraic semantics of a deductive system was proposed in [3], and a preliminary study was begun. The focus of [3] was the definition and investigation of algebraizable deductive systems, i.e., the deductive systems that possess an equivalent algebraic semantics. The present paper explores the more general property of possessing an algebraic semantics. While a deductive system can have at most one equivalent algebraic semantics, it may have numerous different algebraic semantics. All of these give (...) rise to an algebraic completeness theorem for the deductive system, but their algebraic properties, unlike those of equivalent algebraic semantics, need not reflect the metalogical properties of the deductive system. Many deductive systems that don't have an equivalent algebraic semantics do possess an algebraic semantics; examples of these phenomena are provided. It is shown that all extensions of a deductive system that possesses an algebraic semantics themselves possess an algebraic semantics. Necessary conditions for the existence of an algebraic semantics are given, and an example of a protoalgebraic deductive system that does not have an algebraic semantics is provided. The mono-unary deductive systems possessing an algebraic semantics are characterized. Finally, weak conditions on a deductive system are formulated that guarantee the existence of an algebraic semantics. These conditions are used to show that various classes of non-algebraizable deductive systems of modal logic, relevance logic and linear logic do possess an algebraic semantics. (shrink)

The three essays presented here concern natural connections between grammatical derivations and structures provided by certain standard grammar formalisms, on the one hand, and deductions in logical systems, on the other hand. In the first essay we analyse the adequacy of Polish notation for higher-order languages. The Ajdukiewicz algorithm (Ajdukiewicz 1935) is discussed in terms of generalized MP-deductions. We exhibit a failure in Ajdukiewicz’s original version of the algorithm and give a correct one; we prove that generalized MP-deductions have the (...) frontier property, which is essential for the plausibility of Polish notation. The second essay deals with logical systems corresponding to different grammar formalisms, as e.g. Finite State Acceptors, Context-Free Grammars, Categorial Grammars, and others. We show how can logical methods be used to establish certain linguistically significant properties of formal grammars. The third essay discusses the interplay between Natural Deduction proofs in grammar oriented logics and semantic structures expressible by typed lambda terms and combinators. (shrink)

Expert Systems (ES) are as yet imperfectly defined. Their two consistently cited characteristics are domain knowledge and expert-level performance. We propose that current structural definitions are inadequate and suggest a view of ES as communication channels. We proceed to explore the factors influencing applicability of ES technology to an enterprise and the impacts that could be expected. A consequence of this view is the idea of incremental information loss on the path from the expert to the ES (...) user. Strategies for minimizing this loss derive naturally from our perspective and are evident in successful ES. (shrink)

We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof (...) is the number of lines in the proof. A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by "nearly linear" is meant the ratio of proof lengths is O) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O lines and of height O. As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O. (shrink)

We present a sound and complete Fitch-style natural deduction system for an S5 modal logic containing an actuality operator, a diagonal necessity operator, and a diagonal possibility operator. The logic is two-dimensional, where we evaluate sentences with respect to both an actual world (first dimension) and a world of evaluation (second dimension). The diagonal necessity operator behaves as a quantifier over every point on the diagonal between actual worlds and worlds of evaluation, while the diagonal possibility quantifies over (...) some point on the diagonal. Thus, they are just like the epistemic operators for apriority and its dual. We take this extension of Fitch’s familiar derivation system to be a very natural one, since the new rules and labeled lines hereby introduced preserve the structure of Fitch’s own rules for the modal case. (shrink)

Harold Hodes in [1] introduces an extension of first-order modal logic featuring a backtracking operator, and provides a possible worlds semantics, according to which the operator is a kind of device for ‘world travel’; he does not provide a proof theory. In this paper, I provide a natural deduction system for modal logic featuring this operator, and argue that the system can be motivated in terms of a reading of the backtracking operator whereby it serves to indicate (...) modal scope. I prove soundness and completeness theorems with respect to Hodes’ semantics, as well as semantics with fewer restrictions on the accessibility relation. (shrink)

This is a companion paper to Braüner where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relations and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we prove a normalisation theorem. Moreover, we give an (...) axiom system first-order hybrid logic. (shrink)

We present a sound and complete Fitch-style natural deduction system for an S5 modal logic containing an actuality operator, a diagonal necessity operator, and a diagonal possibility operator. The logic is two-dimensional, where we evaluate sentences with respect to both an actual world (first dimension) and a world of evaluation (second dimension). The diagonal necessity operator behaves as a quantifier over every point on the diagonal between actual worlds and worlds of evaluation, while the diagonal possibility quantifies over (...) some point on the diagonal. Thus, they are just like the epistemic operators for apriority and its dual. We take this extension of Fitch’s familiar derivation system to be a very natural one, since the new rules and labeled lines hereby introduced preserve the structure of Fitch’s own rules for the modal case. (shrink)

Deductive Logic is designed as an intermediate-level text directed at upper-division students from philosophy and the humanities. Its focus is exclusively on deductive logic, avoiding altogether topics such as informal reasoning and scientific method normally included in introductory logic courses. Its exposition of logical topics is informal, with emphasis on explaining the basic concepts and procedures of modern symbolic logic in the simplest and most intuitive manner possible rather than on developing a rigorous formal system and providing proofs of (...) its properties. The fact that the text presupposes a course offered to philosophy students and serves to introduce them to logic as the "language of philosophy" has strongly influenced the selection of topics. The topics here are controversial, and the problems not easily resolved, but this text strives to relate the formal logical structures introduced to issues of philosophic interest. (shrink)

In this paper two deductive systems associated with relevance logic are studied from an algebraic point of view. One is defined by the familiar, Hilbert-style, formalization of R; the other one is a weak version of it, called WR, which appears as the semantic entailment of the Meyer-Routley-Fine semantics, and which has already been suggested by Wójcicki for other reasons. This weaker consequence is first defined indirectly, using R, but we prove that the first one turns out to be an (...) axiomatic extension of WR. Moreover we provide WR with a natural Gentzen calculus. It is proved that both deductive systems have the same associated class of algebras but different classes of models on these algebras. The notion of model used here is an abstract logic, that is, a closure operator on an abstract algebra; the abstract logics obtained in the case of WR are also the models, in a natural sense, of the given Gentzen calculus. (shrink)

It is sometimes objected that Tichý’s logic is not a logic because it underestimates deduction, providing only logical analyses of expressions. I argue that this opinion is wrong. First of all, to detect valid arguments, which are formulated in a language, there needs to be logical analysis to ascertain which semantical entities are involved. Entailment is defined as an extralinguistic affair relating those constructions. The validity of an argument, composed of propositional constructions, stems from the properties of the constructions. (...) Such properties are displayed by the derivation rules of Tichý’s system of deduction. (shrink)

To effectively pursue ethical action, the business community must recognize that the fundamental form of human association is not the "social contract" into which persons enter as atomic individuals, making partial commitments to each other for the purpose of gaining limited common ends or of satisfying certain laws. The fundamental form of human association is rather the face to face community in which ongoing commitments are the rule and in which aspects of every individual''s experience are conditioned by the continuing (...) membership. The following discussion initiates a preliminary phase in the consideration of what constitutes ethical issues associated with the business applications of expert systems. The focus is on knowledge based expert system applications in public accounting, specifically in the audit domain. Prior research on the development and use of expert systems in auditing has focused on a limited set of ethical issues. Niebuhr''s theory of the "the responsible self" is used here to broaden the scope of what constitutes an ethical issue and provides a framework for identifying responsible action. Within this framework, an action is responsible if it takes into consideration ongoing relationships among the stakeholder groups affected. Actions prior to the development of the system along with the potential consequences for the system must be considered. The discursive requirements that provide the context and conditions necessary for implementing the proposed theoretical framework are presented and an illustration of how the responsibility ethic can be implemented in the audit expert system domain is developed. (shrink)

Extant semantic theories for languages containing vague expressions violate intuition by delivering the same verdict on two principles of classical propositional logic: the law of noncontradiction and the law of excluded middle. Supervaluational treatments render both valid; many-Valued treatments, Neither. The core of this paper presents a natural deduction system, Sound and complete with respect to a 'mixed' semantics which validates the law of noncontradiction but not the law of excluded middle.

We can formalize judgments as logical formulas. Judgment aggregation deals with judgments of several agents, which need to be aggregated to a collective judgment. There are several logical formalizations of judgment aggregation. This paper focuses on a modal formalization which nicely expresses classical properties of judgment aggregation rules and famous results of social choice theory, like Arrow’s impossibility theorem. A natural deduction system for modal logic of judgment aggregation is presented in this paper. The system is sound (...) and complete. As an example of derivation, a formal proof of Arrow’s impossibility theorem is given. (shrink)

Deductive proof checking programs are the most popular form of logic CAI. Whatever the reason for their widespread use, the proliferation and continuous development of these programs is evident. Contemporary proof checkers cover a wider variety of texts and rule sets, and offer more helpful editing, diagnostic, and remedial features than were once provided. These programs appear to be prime candidates for developing in the direction of "intelligent" CAI (ICAI). The primary thrust of ICAI is to build programs that make (...) use of information about learner strengths and weaknesses, the content of the subject matter being taught, and techniques for teaching various kinds of subject matter. This is a tall order by any standard, but there are signs that some initial progress is being made in the area of logic CAI. In particular, the expert system approach for offering strategic advice during proof construction is being explored by some projects. (shrink)

This article examines Quine's original proposal for a natural deduction calculus including an existential specification rule, it argues that it introduces a new paradigm of natural deduction alternative to Gentzen's but has some substantial defects. As an alternative the article puts forward a system of sequent natural deduction.

In this paper we consider the structure of the class FGModS of full generalized models of a deductive system S from a universal-algebraic point of view, and the structure of the set of all the full generalized models of S on a fixed algebra A from the lattice-theoretical point of view; this set is represented by the lattice FACSs A of all algebraic closed-set systems C on A such that (A, C) ε FGModS. We relate some properties of these (...) structures with tipically logical properties of the sentential logic S. The main algebraic properties we consider are the closure of FGModS under substructures and under reduced products, and the property that for any A the lattice FACSs A is a complete sublattice of the lattice of all algebraic closed-set systems over A. The logical properties are the existence of a fully adequate Gentzen system for S, the Local Deduction Theorem and the Deduction Theorem for S. Some of the results are established for arbitrary deductive systems, while some are found to hold only for deductive systems in more restricted classes like the protoalgebraic or the weakly algebraizable ones. The paper ends with a section on examples and counterexamples. (shrink)