Principal type-schemes and condensed detachment

1990 ◽  
Vol 55 (1) ◽  
pp. 90-105 ◽  
Author(s):  
J. Roger Hindley ◽  
David Meredith
Keyword(s):  
Type Theory ◽  
Propositional Logic ◽  
Modus Ponens ◽  
The Other ◽  
Combinatory Logic ◽  
Minimal Amount ◽  
Principal Type ◽  
Condensed Detachment

The condensed detachment rule, or ruleD, was first proposed by Carew Meredith in the 1950's for propositional logic based on implication. It is a combination of modus ponens with a “minimal” amount of substitution. We shall give a precise detailed statement of rule D. (Some attempts in the published literature to do this have been inaccurate.)The D-completeness question for a given set of logical axioms is whether every formula deducible from the axioms by modus ponens and substitution can be deduced instead by rule D alone. Under the well-known formulae-as-types correspondence between propositional logic and combinator-based type-theory, rule D turns out to correspond exactly to an algorithm for computing principal type-schemes in combinatory logic. Using this fact, we shall show that D is complete for intuitionistic and classical implicational logic. We shall also show that D is incomplete for two weaker systems, BCK- and BCI-logic.In describing the formulae-as-types correspondence it is common to say that combinators correspond to proofs in implicational logic. But if “proofs” means “proofs by the usual rules of modus ponens and substitution”, then this is not true. It only becomes true when we say “proofs by rule D”; we shall describe the precise correspondence in Corollary 6.7.1 below.This paper is written for readers in propositional logic and in combinatory logic. Since workers in one field may not feel totally happy in the other, we include short introductions to both fields.We wish to record thanks to Martin Bunder, Adrian Rezus and the referee for helpful comments and advice.

scholarly journals Forward and Backward Chaining with P Systems

2014 ◽  
pp. 149-158
Author(s):  
Sergiu Ivanov ◽  
Artiom Alhazov ◽  
Vladimir Rogojin ◽  
Miguel A. Gutiérrez-Naranjo
Keyword(s):  
Computer Science ◽  
Propositional Logic ◽  
Membrane Computing ◽  
Modus Ponens ◽  
The Other ◽  
P Systems ◽  
Backward Chaining ◽  
Other Hand

One of the concepts that lie at the basis of membrane computing is the multiset rewriting rule. On the other hand, the paradigm of rules is profusely used in computer science for representing and dealing with knowledge. Therefore, establishing a “bridge” between these domains is important, for instance, by designing P systems reproducing the modus ponens-based forward and backward chaining that can be used as tools for reasoning in propositional logic. In this paper, the authors show how powerful and intuitive the formalism of membrane computing is and how it can be used to represent concepts and notions from unrelated areas.

Implication with possible exceptions

2001 ◽  
Vol 66 (2) ◽  
pp. 517-535
Author(s):  
Herman Jurjus ◽  
Harrie de Swart
Keyword(s):  
Propositional Logic ◽  
Modus Ponens ◽  
The Other ◽  
Classical Propositional Logic ◽  
Consequence Relation ◽  
Other Hand

AbstractWe introduce an implication-with-possible-exceptions and define validity of rules-with-possible-exceptions by means of the topological notion of a full subset. Our implication-with-possible-exceptions characterises the preferential consequence relation as axiomatized by Kraus, Lehmann and Magidor [Kraus, Lehmann, and Magidor, 1990]. The resulting inference relation is non-monotonic. On the other hand, modus ponens and the rule of monotony, as well as all other laws of classical propositional logic, are valid-up-to-possible exceptions. As a consequence, the rules of classical propositional logic do not determine the meaning of deducibility and inference as implication-without-exceptions.

scholarly journals Forward and Backward Chaining with P Systems

2011 ◽  
Vol 2 (2) ◽  
pp. 56-66 ◽  
Author(s):  
Sergiu Ivanov ◽  
Artiom Alhazov ◽  
Vladimir Rogojin ◽  
Miguel A. Gutiérrez-Naranjo
Keyword(s):  
Computer Science ◽  
Propositional Logic ◽  
Membrane Computing ◽  
Modus Ponens ◽  
The Other ◽  
P Systems ◽  
Backward Chaining ◽  
Other Hand

One of the concepts that lie at the basis of membrane computing is the multiset rewriting rule. On the other hand, the paradigm of rules is profusely used in computer science for representing and dealing with knowledge. Therefore, establishing a “bridge” between these domains is important, for instance, by designing P systems reproducing the modus ponens-based forward and backward chaining that can be used as tools for reasoning in propositional logic. In this paper, the authors show how powerful and intuitive the formalism of membrane computing is and how it can be used to represent concepts and notions from unrelated areas.

scholarly journals Forward and Backward Chaining with P Systems

2012 ◽  
pp. 1522-1531
Author(s):  
Sergiu Ivanov ◽  
Artiom Alhazov ◽  
Vladimir Rogojin ◽  
Miguel A. Gutiérrez-Naranjo
Keyword(s):  
Computer Science ◽  
Propositional Logic ◽  
Membrane Computing ◽  
Modus Ponens ◽  
The Other ◽  
P Systems ◽  
Backward Chaining ◽  
Other Hand

One of the concepts that lie at the basis of membrane computing is the multiset rewriting rule. On the other hand, the paradigm of rules is profusely used in computer science for representing and dealing with knowledge. Therefore, establishing a “bridge” between these domains is important, for instance, by designing P systems reproducing the modus ponens-based forward and backward chaining that can be used as tools for reasoning in propositional logic. In this paper, the authors show how powerful and intuitive the formalism of membrane computing is and how it can be used to represent concepts and notions from unrelated areas.

Hilbert-style proof Calculus for Propositional Logic in ABC notation

2019 ◽  
Author(s):  
Matheus Pereira Lobo
Keyword(s):  
Propositional Logic ◽  
Inference Rule ◽  
Modus Ponens ◽  
Axiomatic System ◽  
First Contact

All nine axioms and a single inference rule of logic (Modus Ponens) within the Hilbert axiomatic system are presented using capital letters (ABC) in order to familiarize the beginner student in hers/his first contact with the topic.

Comparative abilities of thyroxine and triiodothyronine as inhibitors of pituitary thyrotropin secretion in cattle

1961 ◽  
Vol 201 (1) ◽  
pp. 77-80 ◽  
Author(s):  
B. N. Premachandra ◽  
G. W. Pipes ◽  
C. W. Turner
Keyword(s):  
Biological Activity ◽  
Dairy Cows ◽  
Secretion Rate ◽  
The Other ◽  
Minimal Amount ◽  
Holstein Breed ◽  
The Mean

A technique is described using radioactiveiodine (I131) and the goitrogen, Tapazole, in mature dairy cows, to compare the relative biological activity of l-thyroxine (T4) and l-triiodothyronine (T3) in individual animals to inhibit pituitary thyrotropin (TSH) release and, in turn, release of thyroidal-I131. The minimal amount of either hormone required is considered the equivalent T4 or T3 secretion rate. The individuals of the Holstein breed showed a mean molar relation of 1:2.5, which was significantly higher than the means of the other breeds. The mean of 22 animals showed a ratio of 1:2.14, indicating that T3 is slightly over twice as effective as T4 in blocking TSH and thyroidal-I131 release. While T3 is more potent in blocking TSH discharge, it was observed that upon withdrawal of T4 and T3 the resumption of thyroidal-I131 release was more rapid after T3 administration.

scholarly journals ANTIBODY RESPONSE OF PATIENTS WITH POLIOMYELITIS TO VIRUS RECOVERED FROM THEIR OWN ALIMENTARY TRACT

1949 ◽  
Vol 90 (4) ◽  
pp. 349-372 ◽  
Author(s):  
Alex J. Steigman ◽  
Albert B. Sabin
Keyword(s):  
Single Dose ◽  
Antibody Response ◽  
Acute Phase ◽  
Alimentary Tract ◽  
High Titer ◽  
The Other ◽  
Minimal Amount ◽  
Virus Antibody ◽  
Serum Dilution

Of 20 strains of virus recovered from 40 patients with poliomyelitis only 9 possessed a titer of 10–3 or more, permitting significant quantitative neutralization tests in monkeys. Seven of the 9 high titer strains were derived from patients whose illness was ultimately paralytic, and tests with their undiluted sera indicated that the acute phase as well as the 3 month convalescent specimens neutralized maximum amounts of the patient's own virus. However when varying dilutions of the sera were tested against a single dose of virus, it was found that the antibody was present in lowest concentration early after onset and progressively increased in titer over a period of weeks during convalescence. The 2 remaining high titer strains were recovered from patients with a non-paralytic illness, and in both of these the acute phase sera were without significant amounts of antibody for their own virus. Antibody was demonstrable at 14, 28, and 92 days after onset in one of these patients, while the other had none at 1 month and only a minimal amount at 3 and 8 months. Tests with the Lansing virus on the same sera, clearly established the specificity of the antibody response to the strain of virus recovered from each patient under investigation. Five of the 9 patients, whose sera were studied with both viruses, had no antibody for the Lansing virus during the acute phase and none 3 months later. Two had antibody during the acute phase but serum dilution tests showed no increase in titer in the 3 month convalescent specimen. In 2 others, who were without antibody for the Lansing virus during the acute phase but had it at 3 months after onset, it was possible to show that this antibody appeared later than 1 month after the illness and that the virus recovered from these patients during their illness was not antigenically of the Lansing type.

Reducibilities in two models for combinatory logic

1979 ◽  
Vol 44 (2) ◽  
pp. 221-234 ◽  
Author(s):  
Luis E. Sanchis
Keyword(s):  
Recursive Function ◽  
Present Method ◽  
Function Theory ◽  
Graph Model ◽  
The Other ◽  
Combinatory Logic ◽  
General Properties ◽  
Hypergraph Model ◽  
Natural Frame ◽  
Natural Way

This paper proposes a generalization of several reducibilities in the sense of recursive function theory. For this purpose two structures are introduced as models of combinatory logic and reducibilities are defined in a rather natural way by means of the application operation in each model. The first model we consider is called the graph model and was introduced by Dana Scott in [11]. Reducibilities in this model are generalizations of enumeration and Turing reducibilities. The second model is called the hypergraph model and induces reducibilities which are generalizations of hyperenumeration and hyperarithmetical reducibilities.The possibility of formulating reducibilities in this way is not new. For the graph model it is implicit in [7] and for the hypergraph model in [9]. On the other hand it is possible to look at the present method as a variant of the well-known technique of relativization in recursive function theory. We think that this does not exhaust the power of the method, which is conceptually elegant and provides a natural frame for the results of this paper.In the first part of the paper we discuss the definition and general properties of the models. Then we introduce the reducibilities in the graph model and prove several theorems which are generalizations of properties already Known for enmeration and Turing reducibilities. Next we define reducibilities in the hypergraph model and try to extend the preceding results. For this purpose we prove two theorems showing significant relations between the operators in both models. In fact we prove that each operator in the hypergraph model can be simulated on a comeager set by an operator of the graph model.

scholarly journals Principal type schemes for an extended type theory

1983 ◽  
Vol 28 (1-2) ◽  
pp. 151-169 ◽  
Author(s):  
S.Ronchi Della Rocca ◽  
B. Venneri
Keyword(s):  
Type Theory ◽  
Principal Type ◽  
Extended Type

The inadequacy of the neighbourhood semantics for modal logic

1975 ◽  
Vol 40 (2) ◽  
pp. 141-148 ◽  
Author(s):  
Martin Gerson
Keyword(s):  
Modal Logic ◽  
Modus Ponens ◽  
The Other ◽  
Montague Semantics ◽  
Propositional Constants

We present two finitely axiomatized modal propositional logics, one between T and S4 and the other an extension of S4, which are incomplete with respect to the neighbourhood or Scott-Montague semantics.Throughout this paper we are referring to logics which contain all the classical connectives and only one modal connective □ (unary), no propositional constants, all classical tautologies, and which are closed under the rules of modus ponens (MP), substitution, and the rule RE (from A ↔ B infer αA ↔ □B). Such logics are called classical by Segerberg [6]. Classical logics which contain the formula □p ∧ □q → □(p ∧ q) (denoted by K) and its “converse,” □{p ∧ q)→ □p ∧ □q (denoted by R) are called regular; regular logics which are closed under the rule of necessitation, RN (from A infer □A), are called normal. The logics that we are particularly concerned with are all normal, although some of our results will be true for all regular or all classical logics. It is well known that K and R and closure under RN imply closure under RE and also that normal logics are also those logics closed under RN and containing □{p → q) → {□p → □q).

Sign in / Sign up

Export Citation Format

Share Document