The complexity of decision procedures in relevance logic II

1999 ◽  
Vol 64 (4) ◽  
pp. 1774-1802 ◽  
Author(s):  
Alasdair Urquhart
Keyword(s):  
Lower Bound ◽  
Decision Problem ◽  
Decision Procedure ◽  
Linear Logic ◽  
Decision Procedures ◽  
Search Tree ◽  
Saul Kripke ◽  
Decision Method ◽  
Relevant Logics ◽  
Primitive Recursive

In this paper, we show that there is no primitive recursive decision procedure for the implication-conjunction fragments of the relevant logics R, E and T, as well as for a family of related logics. The lower bound on the complexity is proved by combining the techniques of an earlier paper on the same subject [20] with a method used by Lincoln, Mitchell, Scedrov and Shankar in proving that propositional linear logic is undecidable.The decision problem for the pure implicational fragments of E and R were solved by Saul Kripke in a tour de force of combinatorial reasoning, published only as an abstract [9]. Belnap and Wallace extended Kripke's decision procedure to the implication-negation fragment of E in [3]; an account of their decision method is to be found in [1, pp. 124–139]. The decision method extends immediately to the implication/negation fragment of R. In fact, in the case of R we can go farther: Meyer in his thesis [13] showed how to translate the logic LR, which results from R by omitting the distribution axiom, into R→⋀, so that the decision procedure can be extended to all of LR. This decision procedure has been implemented as a program Kripke by Thistlewaite, McRobbie and Meyer [17]. The program is not simply a straightforward implementation of the decision procedure; finite matrices are used extensively to prune invalid nodes from the search tree.

On the Gödel class with identity

1981 ◽  
Vol 46 (2) ◽  
pp. 354-364 ◽  
Author(s):  
Warren D. Goldfarb
Keyword(s):  
Recursive Function ◽  
Decision Problem ◽  
Decision Procedure ◽  
Finite Model ◽  
Quantification Theory ◽  
Free Variables ◽  
Primitive Recursive

The Gödel Class is the class of prenex formulas of pure quantification theory whose prefixes have the form ∀y1∀y2∃x1 … ∃xn. The Gödel Class with Identity, or GCI, is the corresponding class of formulas of quantification theory extended by inclusion of the identity-sign “ = ”. Although the Gödel Class has long been kndwn to be solvable, the decision problem for the Gödel Class with Identity is open. In this paper we prove that there is no primitive recursive decision procedure for the GCI, or, indeed, for the subclass of the GCI containing just those formulas with prefixes ∀y1∀y2∃x.Throughout this paper we take quantification theory to include, aside from logical signs, infinitely many k-place predicate letters for each k > 0, but no function signs or constants. Moreover, by “prenex formula” we include only those without free variables. A decision procedure for a class of formulas is a recursive function that carries a formula in the class to 0 if the formula is satisfiable and to 1 if not. A class is solvable iff there exists a decision procedure for it. A class is finitely controllable iff every satisfiable formula in the class has a finite model. Since we speak only of effectively specified classes, finite controllability implies solvability (but not conversely).The GCI has a curious history. Gödel showed the Gödel Class (without identity) solvable in 1932 [4] and finitely controllable in 1933 [5].

Deciding Clause Classes by Semantic Clash Resolution

1993 ◽  
Vol 18 (2-4) ◽  
pp. 163-182
Author(s):  
Alexander Leitsch
Keyword(s):  
Decision Procedure ◽  
Decision Procedures ◽  
General Concept ◽  
Complexity Measure ◽  
Syntactical Structure

It is investigated, how semantic clash resolution can be used to decide some classes of clause sets. Because semantic clash resolution is complete, the termination of the resolution procedure on a class Γ gives a decision procedure for Γ. Besides generalizing earlier results we investigate the relation between termination and clause complexity. For this purpose we define the general concept of atom complexity measure and show some general results about termination in terms of such measures. Moreover, rather than using fixed resolution refinements we define an algorithmic generator for decision procedures, which constructs appropriate semantic refinements out of the syntactical structure of the clause sets. This method is applied to the Bernays – Schönfinkel class, where it gives an efficient (resolution) decision procedure.

Comparison of Judgment Scales of the Analytical Hierarchy Process — A New Approach

2019 ◽  
Vol 18 (02) ◽  
pp. 445-463 ◽  
Author(s):  
Klaus D. Goepel
Keyword(s):  
Analytical Hierarchy Process ◽  
Analytic Functions ◽  
Decision Problem ◽  
Decision Criteria ◽  
Maximum Weight ◽  
Analytic Hierarchy ◽  
New Approach ◽  
Scale Functions ◽  
Decision Method ◽  
Hierarchy Process

The analytic hierarchy process (AHP) remains a popular multi-criteria decision method. One topic under discussion of AHP is the use of different scales to translate judgments into ratios. The author makes a new approach to compare different scale functions and to derive a recommendation for the application of scales. The approach is based on simple analytic functions and takes into consideration the number of criteria of the decision problem. A generalization of the so-called balanced scale is proposed, and a new adaptive-balanced scale is introduced. Scales are then categorized and compared based on weight boundaries and weight ratios, weight uncertainties, weight dispersion and number of decision criteria. Finally, a practical example of a decision hierarchy is presented applying the different scales. The results show that the generalized balanced scale improves weight dispersion and weight uncertainty in comparison to the fundamental AHP scale. The proposed adaptive-balanced scale overcomes the problem of a change of the maximum weight depending on the number of decision criteria.

Trial and error predicates and the solution to a problem of Mostowski

1965 ◽  
Vol 30 (1) ◽  
pp. 49-57 ◽  
Author(s):  
Hilary Putnam
Keyword(s):  
Finite Number ◽  
Correct Answer ◽  
Decision Procedure ◽  
Finite Sequence ◽  
Decision Procedures ◽  
Turing Machines ◽  
Trial And Error ◽  
Church’S Thesis ◽  
Church's Thesis ◽  
Empirical Means

The purpose of this paper is to present two groups of results which have turned out to have a surprisingly close interconnection. The first two results (Theorems 1 and 2) were inspired by the following question: we know what sets are “decidable” — namely, the recursive sets (according to Church's Thesis). But what happens if we modify the notion of a decision procedure by (1) allowing the procedure to “change its mind” any finite number of times (in terms of Turing Machines: we visualize the machine as being given an integer (or an n-tuple of integers) as input. The machine then “prints out” a finite sequence of “yesses” and “nos”. The last “yes” or “no” is always to be the correct answer.); and (2) we give up the requirement that it be possible to tell (effectively) if the computation has terminated? I.e., if the machine has most recently printed “yes”, then we know that the integer put in as input must be in the set unless the machine is going to change its mind; but we have no procedure for telling whether the machine will change its mind or not.The sets for which there exist decision procedures in this widened sense are decidable by “empirical” means — for, if we always “posit” that the most recently generated answer is correct, we will make a finite number of mistakes, but we will eventually get the correct answer. (Note, however, that even if we have gotten to the correct answer (the end of the finite sequence) we are never sure that we have the correct answer.)

scholarly journals ON THE FINITENESS PROBLEM FOR AUTOMATON (SEMI)GROUPS

2012 ◽  
Vol 22 (06) ◽  
pp. 1250052 ◽  
Author(s):  
ALI AKHAVI ◽  
INES KLIMANN ◽  
SYLVAIN LOMBARDY ◽  
JEAN MAIRESSE ◽  
MATTHIEU PICANTIN
Keyword(s):  
Decision Problem ◽  
Decision Procedure ◽  
Necessary Condition ◽  
Sufficient Condition ◽  
Necessary And Sufficient Condition ◽  
Mealy Automata ◽  
Necessary And Sufficient ◽  
New Criteria

This paper addresses a decision problem highlighted by Grigorchuk, Nekrashevich, and Sushchanskiĭ, namely the finiteness problem for automaton (semi)groups. For semigroups, we give an effective sufficient but not necessary condition for finiteness and, for groups, an effective necessary but not sufficient condition. The efficiency of the new criteria is demonstrated by testing all Mealy automata with small stateset and alphabet. Finally, for groups, we provide a necessary and sufficient condition that does not directly lead to a decision procedure.

An estimate of mean efficiency of search trees for arbitrary sets of binary words

2002 ◽  
Vol 12 (2) ◽  
Author(s):  
B.Ya. Ryabko ◽  
A.A. Fedotov
Keyword(s):  
Lower Bound ◽  
Search Tree ◽  
Binary Search ◽  
Binary Search Tree ◽  
Minimal Cost ◽  
Search Trees ◽  
Optimal Tree ◽  
Np Complete ◽  
The Mean ◽  
Binary Logarithm

AbstractWe consider the problem on constructing a binary search tree for an arbitrary set of binary words, which has found a wide use in informatics, biology, mineralogy, and other fields. It is known that the problem on constructing the tree of minimal cost is NP-complete; hence the problem arises to find simple algorithms which allow us to construct trees close to the optimal ones. In this paper we demonstrate that even simplest algorithm yields search trees which are close to the optimal ones in average, and prove that the mean number of nodes checked in the optimal tree differs from the natural lower bound, the binary logarithm of the number of words, by no more than 1.04.

scholarly journals A DECISION PROBLEM FOR ULTIMATELY PERIODIC SETS IN NONSTANDARD NUMERATION SYSTEMS

2009 ◽  
Vol 19 (06) ◽  
pp. 809-839 ◽  
Author(s):  
JASON BELL ◽  
EMILIE CHARLIER ◽  
AVIEZRI S. FRAENKEL ◽  
MICHEL RIGO
Keyword(s):  
Finite Automaton ◽  
Regular Language ◽  
Decision Problem ◽  
Decision Procedure ◽  
Fibonacci Sequence ◽  
Finite Union ◽  
Numeration System ◽  
Periodic Sets ◽  
Numeration Systems ◽  
The One

Consider a nonstandard numeration system like the one built over the Fibonacci sequence where nonnegative integers are represented by words over {0,1} without two consecutive 1. Given a set X of integers such that the language of their greedy representations in this system is accepted by a finite automaton, we consider the problem of deciding whether or not X is a finite union of arithmetic progressions. We obtain a decision procedure for this problem, under some hypothesis about the considered numeration system. In a second part, we obtain an analogous decision result for a particular class of abstract numeration systems built on an infinite regular language.

Decision problems for multiple successor arithmetics

1966 ◽  
Vol 31 (2) ◽  
pp. 182-190 ◽  
Author(s):  
J. W. Thatcher
Keyword(s):  
Decision Problem ◽  
Decision Procedure ◽  
Decision Problems ◽  
First Order

Let Nk denote the set of words over the alphabet Σk = {1, …, k}. Nk contains the null word which is denoted λ. We consider decision problems for various first-order interpreted predicate languages in which the variables range over Nk (k ≧ 2). Our main result is that there is no decision procedure for truth in the interpreted language which has the subword relation as its only non-logical primitive. This, together with known results summarized in Section 4, settles the decision problem for any language constructed on the basis of the relations and functions listed below.

Sign in / Sign up

Export Citation Format

Share Document