scholarly journals Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus

2007 ◽  
pp. 147-161 ◽  
Author(s):  
Robert Constable ◽  
Wojciech Moczydłowski
Keyword(s):  
Propositional Calculus ◽  
Completeness Proof ◽  
Resolution Algorithm

The completeness of the first-order functional calculus

1949 ◽  
Vol 14 (3) ◽  
pp. 159-166 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Propositional Calculus ◽  
Higher Order ◽  
New Method ◽  
Completeness Proof ◽  
New Approach ◽  
First Order ◽  
Formal Systems ◽  
The Subject ◽  
Image Position

Although several proofs have been published showing the completeness of the propositional calculus (cf. Quine (1)), for the first-order functional calculus only the original completeness proof of Gödel (2) and a variant due to Hilbert and Bernays have appeared. Aside from novelty and the fact that it requires less formal development of the system from the axioms, the new method of proof which is the subject of this paper possesses two advantages. In the first place an important property of formal systems which is associated with completeness can now be generalized to systems containing a non-denumerable infinity of primitive symbols. While this is not of especial interest when formal systems are considered as logics—i.e., as means for analyzing the structure of languages—it leads to interesting applications in the field of abstract algebra. In the second place the proof suggests a new approach to the problem of completeness for functional calculi of higher order. Both of these matters will be taken up in future papers.The system with which we shall deal here will contain as primitive symbolsand certain sets of symbols as follows:(i) propositional symbols (some of which may be classed as variables, others as constants), and among which the symbol “f” above is to be included as a constant;(ii) for each number n = 1, 2, … a set of functional symbols of degree n (which again may be separated into variables and constants); and(iii) individual symbols among which variables must be distinguished from constants. The set of variables must be infinite.

A Gentzen- or Beth-type system, a practical decision procedure and a constructive completeness proof for the counterfactual logics VC and VCS

1983 ◽  
Vol 48 (1) ◽  
pp. 1-20 ◽  
Author(s):  
H. C. M. de Swart
Keyword(s):  
Decision Procedure ◽  
Type System ◽  
Propositional Calculus ◽  
Axiom System ◽  
Completeness Proof ◽  
Counterfactual Conditional ◽  
System A ◽  
Counterfactual Logic ◽  
Classical Propositional Calculus

In [1] and [2] D. Lewis formulates his counterfactual logic VC as follows. The language contains the connectives ∧, ∨, ⊃, ¬ and the binary connective ≤. A ≤ B is read as “A is at least as possible as B”. The following connectives are defined in terms of ≤.A < B: = ¬(B ≤ A) (it is more possible that A than that B).◊ A ≔ ¬(⊥ ≤ A) (⊥ is the false formula; A is possible).□ A ≔ ⊥ ≤ ¬A (A is necessary). (if A were the case, then B would be the case). (if A were the case, then B might be the case). and are two counterfactual conditional operators. (AB) iff ¬(A ¬B).The following axiom system VC is presented by D. Lewis in [1] and [2]: V: (1) Truthfunctional classical propositional calculus.

Effect of spatial resolution, algorithm and variable set on the estimated distribution of a mammal of concern: the squirrel Sciurus aberti

Ecoscience ◽  
2020 ◽  
Vol 27 (3) ◽  
pp. 195-207 ◽  
Author(s):  
Sarahi Sandoval ◽  
Celia López-González ◽  
Jonathan G. Escobar-Flores ◽  
Raúl O. Martínez-Rincón
Keyword(s):  
Spatial Resolution ◽  
Resolution Algorithm

High-resolution algorithm for fan beam-CT system

1986 ◽  
Vol 17 (7) ◽  
pp. 19-29
Author(s):  
Isao Horiba ◽  
Shigenobu Yanaka ◽  
Akira Iwata ◽  
Nobuo Suzumura
Keyword(s):  
High Resolution ◽  
Resolution Algorithm ◽  
Ct System

An algebraic study of Diodorean modal systems

1965 ◽  
Vol 30 (1) ◽  
pp. 58-64 ◽  
Author(s):  
R. A. Bull
Keyword(s):  
Discrete Time ◽  
Decision Procedure ◽  
John Locke ◽  
Original Model ◽  
Completeness Proof ◽  
Semantic Tableaux ◽  
Algebraic Treatment ◽  
Algebraic Result ◽  
Modal Systems

Attention was directed to modal systems in which ‘necessarily α’ is interpreted as ‘α. is and always will be the case’ by Prior in his John Locke Lectures of 1956. The present paper shows that S4.3, the extension of S4 withALCLpLqLCLqLp,is complete with respect to this interpretation when time is taken to be continuous, and that D, the extension of S4.3 withALNLpLCLCLCpLpLpLp,is complete with respect to this interpretation when time is taken to be discrete. The method employed depends upon the application of an algebraic result of Garrett Birkhoff's to the models for these systems, in the sense of Tarski.A considerable amount of work on S4.3 and D precedes this paper. The original model with discrete time is given in Prior's [7] (p. 23, but note the correction in [8]); that taking time to be continuous yields a weaker system is pointed out by him in [9]. S4.3 and D are studied in [3] of Dummett and Lemmon, where it is shown that D includes S4.3 andCLCLCpLpLpCMLpLp.While in Oxford in 1963, Kripke proved that these were in fact sufficient for D, using semantic tableaux. A decision procedure for S4.3, using Birkhoff's result, is given in my [2]. Dummett conjectured, in a conversation, that taking time to be continuous yielded S4.3. Thus the originality of this paper lies in giving a suitable completeness proof for S4.3, and in the unified algebraic treatment of the systems. It should be emphasised that the credit for first axiomatising D belongs to Kripke.

Sign in / Sign up

Export Citation Format

Share Document