REVIEW OF: Automated Development of Fundamental Mathematical Theories by Art Quaife. (1992: Kluwer Academic Publishers) 271pp. Using the theorem prover OTTER Art Quaife has proved four hundred theorems of von Neumann-Bernays-Gödel set theory; twelve hundred theorems and definitions of elementary number theory; dozens of Euclidean geometry theorems; and Gödel's incompleteness theorems. It is an impressive achievement. To gauge its significance and to see what prospects it offers this review looks closely at the book and the proofs it presents.

We prove constructively that for any propositional formula in Conjunctive Normal Form, we can either find a satisfying assignment of true and false to its variables, or a refutation of showing that it is unsatisfiable. This refutation is a resolution proof of ¬. From the formalization of our proof in Coq, we extract Robinson’s famous resolution algorithm as a Haskell program correct by construction. The account is an example of the genre of highly readable formalized mathematics.

We present a formalization of first-order predicate calculus with equality which, unlike traditional systems with axiom schemata or substitution rules, is finitely axiomatized in the sense that each step in a formal proof admits only finitely many choices. This formalization is primarily based on the inference rule of condensed detachment of Meredith. The usual primitive notions of free variable and proper substitution are absent, making it easy to verify proofs in a machine-oriented application. Completeness results are presented. The example of (...) Zermelo-Fraenkel set theory is shown to be finitely axiomatized under the formalization. The relationship with resolution-based theorem provers is briefly discussed. A closely related axiomatization of traditional predicate calculus is shown to be complete in a strong metamathematical sense. (shrink)

This paper describes Peirce's systems of logic diagrams, focusing on the so-called ''existential'' graphs, which are equivalent to the first-order predicate calculus. It analyses their implications for the nature of mental representations, particularly mental models with which they have many characteristics in common. The graphs are intended to be iconic, i.e., to have a structure analogous to the structure of what they represent. They have emergent logical consequences and a single graph can capture all the different ways in which a (...) possibility can occur. Mental models share these properties. But, as the graphs show, certain aspects of propositions cannot be represented in an iconic or visualisable way. They include negation, and the representation of possibilities qua possibilities, which both require representations that do not depend on a perceptual modality. Peirce took his graphs to reveal the fundamental operations of reasoning, and the paper concludes with an analysis of different hypotheses about these operations. (shrink)

In our 2015 book Imagination and Convention, we explore the scope and limits of linguistic knowledge in semantics and pragmatics for natural language. We draw heavily on the notion of coordination from David Lewis' book on conventions. To the extent that the account we develop is right, general principles like Grice's cooperative principle and the maxims of conversation have little to say about about interpretation. Three commentators—Anne Bezuidenhout, Laurence Horn, and Zoltan Gendler Szabo—discuss and evaluate our program in three essays (...) in this issue. What follows is our response to their challenges. (shrink)

We establish a connection between the geometric methods developed in the combinatorial theory of small cancellation and the propositional resolution calculus. We define a precise correspondence between resolution proofs in logic and diagrams in small cancellation theory, and as a consequence, we derive that a resolution proof is a 2-dimensional process. The isoperimetric function defined on diagrams corresponds to the length of resolution proofs.

This article answers two questions (posed in the literature), each concerning the guaranteed existence of proofs free of double negation. A proof is free of double negation if none of its deduced steps contains a term of the formn(n(t)) for some term t, where n denotes negation. The first question asks for conditions on the hypotheses that, if satisfied, guarantee the existence of a double-negation-free proof when the conclusion is free of double negation. The second question asks about the existence (...) of an axiom system for classical propositional calculus whose use, for theorems with a conclusion free of double negation, guarantees the existence of a double-negation-free proof. After giving conditions that answer the first question, we answer the second question by focusing on the Lukasiewicz three-axiom system. We then extend our studies to infinite-valued sentential calculus and to intuitionistic logic and generalize the notion of being double-negation free. The double-negation proofs of interest rely exclusively on the inference rule condensed detachment, a rule that combines modus ponens with an appropriately general rule of substitution. The automated reasoning program Otter played an indispensable role in this study. (shrink)

Despite a renewed interest in Richard Angell’s logic of analytic containment ), the first semantics for \ introduced by Fabrice Correia has remained largely unexamined. This paper describes a reasonable approach to Correia semantics by means of a correspondence with a nine-valued semantics for \. The present inquiry employs this correspondence to provide characterizations of a number of propositional logics intermediate between \ and classical logic. In particular, we examine Correia’s purported characterization of classical logic with respect to his semantics, (...) showing the condition Correia cites in fact characterizes the “logic of paradox” \ and provide a correct characterization. Finally, we consider some remarks on related matters, such as the applicability of the present correspondence to the analysis of the system \ and an intriguing relationship between Correia’s models and articular models for first degree entailment. (shrink)

We argue that an adequate treatment of verb phrase anaphora must depart in two major respects from the standard approaches. First of all, VP anaphors cannot be resolved by simply identifying the anaphoric VP with an antecedent VP. The resolution process must establish a syntactic/semantic parallelism between larger units that the VPs occur in. Secondly, discourse structure has a significant influence on the reference possibilities of VPA. This influence must be accounted for. We propose a treatment which meets these requirements. (...) It builds on a discourse grammar which characterizes discourse cohesion by means of a syntactic/semantic matching procedure which recognizes parallel structures in discourse. It turns out that this independently motivated procedure yields the resolution of VPA as a side effect. (shrink)

This paper presents an algorithm that, given a finite set E of pairs of second-order monadic terms, returns a finite set U of ‘substitution schemata’ such that a substitution unifies E iff it is an instance of some member of U . Moreover, E is unifiable precisely if U is not empty. The algorithm terminates on all inputs, unlike the unification algorithms for second-order monadic terms developed by G. Huet and G. Winterstein. The substitution schemata in U use expressions which (...) represent sets of terms that differ only in how many times designated strings of function constants follow themselves. The substitution schemata may contain unresolved ‘identity restrictions’; consequently, the members of U generally do not characterize all the unifiers of E in a completely explicit way. The algorithm is particularly useful for investigating the complexity of formal proofs. (shrink)

The length of resolution proofs is investigated, relative to the model-theoretic measure of Herband complexity. A concept of resolution deduction is introduced which is somewhat more general than the classical concepts. It is shown that proof complexity is exponential in terms of Herband complexity and that this bound is tight. The concept of R-deduction is extended to FR-deduction, where, besides resolution, a function introduction rule is allowed. As an example, consider the clause P Q: conclude P) Q, where a, f (...) are new function symbols extending Herbrand's universe. P ()Q from Q) and Skolemization). By modification of a construction of Statman it is shown that FR-deductions may be nonelementarily shorter than R-deductions . Finally it is proved that FR-deduction has weaker effects only if clausal logic is restricted to Horn logic. (shrink)

This is an extended version of the lectures given during the 12-thConference on Applications of Logic in Philosophy and in the Foundationsof Mathematics in Szklarska Poręba. It contains a surveyof modal hybrid logic, one of the branches of contemporary modal logic. Inthe first part a variety of hybrid languages and logics is presented with adiscussion of expressivity matters. The second part is devoted to thoroughexposition of proof methods for hybrid logics. The main point is to showthat application of hybrid logics (...) may remarkably improve the situation inmodal proof theory. (shrink)

I analyze the frame problem and its relation to other epistemological problems for artificial intelligence, such as the problem of induction, the qualification problem and the "general" AI problem. I dispute the claim that extensions to logic (default logic and circumscriptive logic) will ever offer a viable way out of the problem. In the discussion it will become clear that the original frame problem is really a fairy tale: as originally presented, and as tools for its solution are circumscribed by (...) Pat Hayes, the problem is entertaining, but incapable of resolution. The solution to the frame problem becomes available, and even apparent, when we remove artificial restrictions on its treatment and understand the interrelation between the frame problem and the many other problems for artificial epistemology. I present the solution to the frame problem: an adequate theory and method for the machine induction of causal structure. Whereas this solution is clearly satisfactory in principle, and in practice real progress has been made in recent years in its application, its ultimate implementation is in prospect only for future generations of AI researchers. (shrink)

This book aims to lay bare the logical foundations of tractable reasoning. It draws on Marvin Minsky's seminal work on frames, which has been highly influential in computer science and, to a lesser extent, in cognitive science. Only very few people have explored ideas about frames in logic, which is why the investigation in this book breaks new ground. The apparent intractability of dynamic, inferential reasoning is an unsolved problem in both cognitive science and logic-oriented artificial intelligence. By means of (...) a logical investigation of frames and frame concepts, Andreas devises a novel logic of tractable reasoning, called frame logic. Moreover, he devises a novel belief revision scheme, which is tractable for frame logic. These tractability results shed new light on our logical and cognitive means to carry out dynamic, inferential reasoning. Modularity remains central for tractability, and so the author sets forth a logical variant of the massive modularity hypothesis in cognitive science. (shrink)

The topics of structural proof theory and logic programming have influenced each other for more than three decades. Proof theory has contributed the notion of sequent calculus, linear logic, and higher-order quantification. Logic programming has introduced new normal forms of proofs and forced the examination of logic-based approaches to the treatment of bindings. As a result, proof theory has responded by developing an approach to proof search based on focused proof systems in which introduction rules are organized into two alternating (...) phases of rule application. Since the logic programming community can generate many examples and many design goals, the close connections with proof theory have helped to keep proof theory relevant to the general topic of computational logic. (shrink)

One might poetically muse that computers have the essence both of logic and machines. Through the case of the history of Separation Logic, we explore how this assertion is more than idle poetry. Separation Logic works because it merges the software engineer’s conceptual model of a program’s manipulation of computer memory with the logical model that interprets what sentences in the logic are true, and because it has a proof theory which aids in the crucial problem of scaling the reasoning (...) task. Scalability is a central problem, and some would even say the central problem, in appli- cations of logic in computer science. Separation Logic is an interesting case because of its widespread success in verification tools. For these two senses of model—the engineering/conceptual and the logical—to merge in a genuine sense, each must maintain their norms of use from their home disciplines. When this occurs, both the logic and engineering benefit greatly. Seeking this intersection of two different senses of model provides a strategy for how computer scientists and logicians may be successful. Furthermore, the history of Separation Logic for analysing programs provides a novel case for philosophers of science of how software engineers and computer scientists develop models and the components of such models. We provide three contributions: an exploration of the extent of models merging that is necessary for success in computer science; an introduction to the technical details of Separation Logic, which can be used for reasoning about other exhaustible resources; and an introduction to the problems, process, and results of computer scientists for those outside the field. (shrink)

We investigate several approaches to resolution based automated theoremproving in classical higher-order logic (based on Church's simply typedλ-calculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews' higher-order resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higher-order E-resolution, and extensional higher-order resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratethe parallels and differences of the extensionality treatment of these approachesand demonstrate that extensional higher-order resolution is the sole approach thatcan completely avoid (...) additional extensionality axioms. (shrink)

We argue that an adequate treatment of verb phrase anaphora must depart in two major respects from the standard approaches. First of all, VP anaphors cannot be resolved by simply identifying the anaphoric VP with an antecedent VP. The resolution process must establish a syntactic/semantic parallelism between larger units that the VPs occur in. Secondly, discourse structure has a significant influence on the reference possibilities of VPA. This influence must be accounted for.We propose a treatment which meets these requirements. It (...) builds on a discourse grammar which characterizes discourse cohesion by means of a syntactic/semantic matching procedure which recognizes parallel structures in discourse. It turns out that this independently motivated procedure yields the resolution of VPA as a side effect. (shrink)

Charles L. Dodgson's reputation as a significant figure in nineteenth-century logic was firmly established when the philosopher and historian of philosophy William Warren Bartley, III published Dodgson's ?lost? book of logic, Part II of Symbolic Logic, in 1977. Bartley's commentary and annotations confirm that Dodgson was a superb technical innovator. In this paper, I closely examine Dodgson's methods and their evolution in the two parts of Symbolic Logic to clarify and justify Bartley's claims. Then, using more recent publications and unpublished (...) letters, I argue that Dodgson approached the elimination problem in class logic differently than his contemporaries, and in doing so, anticipated several important concepts and techniques in automated deductive reasoning. These materials also provide additional insight into his reasons for writing this book. (shrink)

The lambdaPi-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the lambdaPi-calculus and prove the cut-elimination theorem. The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The type-theoretic setting considered (...) here elegantly illustrates the distinction between the processes of normalization in a natural deduction system and cut-elimination in a Gentzen-style sequent calculus. (shrink)

We define an order independent version of default unification on typed feature structures. The operation is one where default information in a feature structure typed with a more specific type, will override default information in a feature structure typed with a more general type, where specificity is defined by the subtyping relation in the type hierarchy. The operation is also able to handle feature structures where reentrancies are default. We provide a formal semantics, prove order independence and demonstrate the utility (...) of this version of default unification in several linguistic applications. First, we show how it can be used to define multiple orthogonal default inheritance in the lexicon in a fully declarative fashion. Secondly, we show how default lexical specifications (introduced via default lexical inheritance) can be made to usefully persist beyond the lexicon and interact with syntagmatic rules. Finally, we outline how persistent default unification might underpin default feature propagation principles and a more restrictive and constraint-based approach to lexical rules. (shrink)

This paper gives a simple, elegant statement of the condensed detachment rule that is independent of most general unifiers and proves that this is equivalent to the longer, more usual, formulation.

This book provides a detailed exposition of one of the most practical and popular methods of proving theorems in logic, called Natural Deduction. It is presented both historically and systematically. Also some combinations with other known proof methods are explored. The initial part of the book deals with Classical Logic, whereas the rest is concerned with systems for several forms of Modal Logics, one of the most important branches of modern logic, which has wide applicability.

In Artificial Intelligence, abduction is often formalized in first-order logic. In this article, we focus on the problem of identifying equivalence of two abductive theories represented in first-order logic. To this end, two definitions of equivalence are given for abduction. Explainable equivalence requires that two abductive theories have the same explainability for any observation. On the other hand, explanatory equivalence guarantees that any observation has exactly the same explanations in each abductive theory. Explanatory equivalence is a stronger notion than explainable (...) equivalence. In first-order logic, explainable equivalence can be veri.ed by the notion of extensional equivalence in default theories, while explanatory equivalence reduces to logical equivalence between background theories. We also show the complexity results for abductive equivalence. (shrink)

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

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

Ulrich (2005) showed that most of the known axiomatisations of the classical equivalence calculus (EC) are D-incomplete, that is, they are not complete with the condensed detachment rule (D) as the primary rule of the proof procedure. He proved that the axiomatisation \(\{EEpEqrErEqp, EEEpppp\}\) by Wajsberg (1937) is D-complete and pointed out a number of D-complete single axioms, including one organic single axiom. In this paper we present new single axioms for EC with the condensed detachment and the reversed condensed (...) detachment rules that form D-complete bases and are organic. (shrink)

An erotetic calculus for a given logic constitutes a sequent-style proof-theoretical formalization of the logic grounded in Inferential Erotetic Logic ). In this paper, a new erotetic calculus for Classical Propositional Logic ), dual with respect to the existing ones, is given. We modify the calculus to obtain complete proof systems for the propositional part of paraconsistent logic CLuN and its extensions CLuNs and mbC. The method is based on dual resolution. Moreover, the resolution rule is non-clausal. According to the (...) authors knowledge, this is the first account of resolution for mbC. Last but not least, as the method is grounded in IEL, it constitutes an important tool for the so-called question-processing. (shrink)

On the basis of a wide range of historical examples various features of axioms are discussed in relation to their use in mathematical practice. A very general framework for this discussion is provided, and it is argued that axioms can play many roles in mathematics and that viewing them as self-evident truths does not do justice to the ways in which mathematicians employ axioms. Possible origins of axioms and criteria for choosing axioms are also examined. The distinctions introduced aim at (...) clarifying discussions in philosophy of mathematics and contributing towards a more refined view of mathematical practice. (shrink)

The k-provability for an axiomatic system A is to determine, given an integer k 1 and a formula in the language of A, whether or not there is a proof of in A containing at most k lines. In this paper we develop a unification-theoretic method for investigating the k-provability problem for Parikh systems, which are first-order axiomatic systems that contain a finite number of axiom schemata and a finite number of rules of inference. We show that the k-provability problem (...) for a Parikh system reduces to a unification problem that is essentially the unification problem for second-order terms. By solving various subproblems of this unification problem , we solve the k- probability problem for a variety of Parikh systems, including several formulations of Peano arithmetic. Our method for investigating the k-provability problem employs algorithms that compute and characterize unifiers. We give some examples of how these algorithms can be used to solve complexity problems other than the k-provability problem. (shrink)

The performance of symbolic inference tasks has long been a challenge to connectionists. In this paper, we present an extended survey of this area. Existing connectionist inference systems are reviewed, with particular reference to how they perform variable binding and rule- based reasoning and whether they involve distributed or localist representations. The bene®ts and disadvantages of different representations and systems are outlined, and conclusions drawn regarding the capabilities of connectionist inference systems when compared with symbolic inference systems or when used (...) for cognitive modelling. q 2001 Elsevier Science Ltd. All rights reserved. (shrink)

In this paper we will see deductive systems for classical propositional and predicate logic in the calculus of structures. Like sequent systems, they have a cut rule which is admissible. Unlike sequent systems, they drop the restriction that rules only apply to the main connective of a formula: their rules apply anywhere deeply inside a formula. This allows to observe very clearly the symmetry between identity axiom and the cut rule. This symmetry allows to reduce the cut rule to atomic (...) form in a way which is dual to reducing the identity axiom to atomic form. We also reduce weakening and even contraction to atomic form. This leads to inference rules that are local: they do not require the inspection of expressions of arbitrary size. (shrink)

Quine has argued that modal logic began with the sin of confusing use and mention. Anderson and Belnap, on the other hand, have offered us a way out through a strategy of nominahzation. This paper reviews the history of Lewis's early work in modal logic, and then proves some results about the system in which "A is necessary" is intepreted as "A is a classical tautology.".

The formalization of abductive reasoning has received increasing attention from logicians. However, few work is found beyond abduction in propositional logic, given that in a first order formalism, the undecidability problem naturally appears, and therefore an abductive problem cannot even be appropriately formulated. Still, many applications in artificial intelligence allow finite domains to work with, and this gives an opportunity to apply abduction in first order logic with restricted domains. In this paper, we present an approach to abductive reasoning in (...) C-structures, first order structures with a finite domain in which each of its elements has a corresponding constant representing its interpretation. By using semantic tableaux with bounded depth, that is, C-tableaux (a modification of N-tableaux, introduced by the authors in previous papers) and δ-resolution calculus, we build an effective procedure for the searching of minimal abductive solutions within the proposed semantics. (shrink)

In this paper we start from the assumption that in a metaphor, or an analogy, some terms belonging to one domain (source domain) are used to refer to objects other than their conventional referents belonging to a possibly different domain (target domain). We describe a formalism, which is based on the First Order Predicate Calculus, for representing the knowledge structure associated with a domain and then develop a theory of Constrained Semantic Transference [CST] which allows the terms and the structural (...) relationships of the source domain to be transferred coherently across to the target domain. We show how metaphors and analogies can be characterized in CST in such a way that many of their cognitive properties con be explained.We then propose a theory of Approximate Semantic Transference [AST] which is a computational version of CST and is derived from it by replacing the coherency requirement with approximate coherency. We show how AST can be used as a basis for designing models of cognitive processes involved in comprehending metaphors and analogies. (shrink)

We show that the E + -class can be decided by resolution using a liftable order, when the order is applied a posteriori. This is a surprising result, because the decision procedure for the E + -class was one of the motivations for the study of non-liftable orders. Also surprising is the behaviour of the resolution process. Initially the maximal depth at which a variable occurs can increase, but it will not increase more than a certain bound. We do not (...) make use of any type of saturation rule in our resolution strategy. (shrink)

To adequately model mathematical arguments the analyst must be able to represent the mathematical objects under discussion and the relationships between them, as well as inferences drawn about these objects and relationships as the discourse unfolds. We introduce a framework with these properties, which has been used to analyse mathematical dialogues and expository texts. The framework can recover salient elements of discourse at, and within, the sentence level, as well as the way mathematical content connects to form larger argumentative structures. (...) We show how the framework might be used to support computational reasoning, and argue that it provides a more natural way to examine the process of proving theorems than do Lamport’s structured proofs. (shrink)