On some Alleged Decision Procedures for S4

1966 ◽  
Vol 31 (4) ◽  
pp. 641-643
Author(s):  
Hanson Willam H.
Keyword(s):  
Decision Procedure ◽  
Present Note ◽  
Decision Procedures ◽  
Correct Decision

In [1] Anderson gave what he claimed was a decision procedure for Lewis's calculus S4. One of the proofs of [1] was faulty, however, and he sought to remedy the situation in [2] by modifying slightly one of the conditions of the decision procedure of [1]. Poliferno subsequently reported in [5] that, according to Anderson, the procedure of [2] was not adequate either, but tha t a correct decision procedure for S4 could be obtained by combining the procedures of [1] and [2]. The purpose of the present note is to show tha t none of the three procedures referred to above are correct decision procedures for S4.

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.

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.)

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.

scholarly journals Multiple-Decision Procedures for Testing the Homogeneity of Mean forkExponential Distributions

2014 ◽  
Vol 2014 ◽  
pp. 1-5
Author(s):  
Han-Ching Chen ◽  
Her Pei Shan ◽  
Nae-Sheng Wang
Keyword(s):  
Sample Size ◽  
Null Hypothesis ◽  
Subset Selection ◽  
Critical Value ◽  
Decision Procedures ◽  
Correct Decision ◽  
Exponential Distributions ◽  
Homogeneity Of Variances ◽  
Random Samples ◽  
The Common

In multiple-decision procedures, a crucial objective is to determine the association between the probability of a correct decision (CD) and the sample size. A review of some methods is provided, including a subset selection formulation proposed by Huang and Panchapakesan, a multidecision procedure for testing the homogeneity of means by Huang and Lin, and a similar procedure for testing the homogeneity of variances by Lin and Huang. In this paper, we focus on the use of the Lin and Huang method for testing the null hypothesisH0of homogeneity of means forkexponential distributions. We discuss the decision ruleR, evaluation of the critical valueC, and the infimum ofP(CD∣R)forkindependent random samples fromkexponential distributions. In addition, we also observed that a lower bound for the probability of CD relative to the number of the common sample size is determined based on the desired probability of CD when the largest mean is sufficiently larger than the other means. We explain the results by using two examples.

scholarly journals DEMOCRACY ISN'T THAT SMART (BUT WE CAN MAKE IT SMARTER): ON LANDEMORE'S DEMOCRATIC REASON

Episteme ◽  
2016 ◽  
Vol 14 (2) ◽  
pp. 161-175 ◽  
Author(s):  
Aaron Ancell
Keyword(s):  
Decision Procedure ◽  
Group Performance ◽  
Collective Intelligence ◽  
Decision Procedures ◽  
Recent Book ◽  
Cognitive Diversity ◽  
Individual Ability ◽  
The Individual ◽  
Average Individual ◽  
Better Than

AbstractIn her recent book, Democratic Reason, Hélène Landemore argues that, when evaluated epistemically, “a democratic decision procedure is likely to be a better decision procedure than any non-democratic decision procedures, such as a council of experts or a benevolent dictator” (p. 3). Landemore's argument rests heavily on studies of collective intelligence done by Lu Hong and Scott Page. These studies purport to show that cognitive diversity – differences in how people solve problems – is actually more important to overall group performance than average individual ability – how smart the individual members are. Landemore's argument aims to extrapolate from these results to the conclusion that democracy is epistemically better than any non-democratic rival. I argue here that Hong and Page's results actually undermine, rather than support, this conclusion. More specifically, I argue that the results do not show that democracy is better than any non-democratic alternative, and that in fact, they suggest the opposite – that at least some non-democratic alternatives are likely to epistemically outperform democracy.

Automating assistance for safety critical decisions

1990 ◽  
Vol 327 (1241) ◽  
pp. 555-567 ◽  
Keyword(s):  
Decision Making ◽  
Decision Procedure ◽  
Predicate Logic ◽  
Decision Procedures ◽  
Statistical Decision ◽  
Unpredictable Environments ◽  
Human Decision ◽  
Human Operators ◽  
Classical Decision ◽  
Special Case

Computer systems are increasingly being introduced to assist in decision making, including hazardous decision making. To ensure effective assistance, decision procedures should be theoretically sound, flexible in operation (particularly in unpredictable environments) and effectively accountable to human supervisors and auditors. Strengths and weaknesses of classical statistical decision models are discussed from these perspectives. It is argued that more can be learned from human decision behaviour than has traditionally been assumed, and this motivates the concept of a symbolic decision procedure (SDP). The SDP is defined, described in terms of first-order (predicate) logic, and its use illustrated in a decision support system for medicine. We point out that the classical numerical decision procedure is a special case of a generalized symbolic procedure, and discuss the potential for rigorous formalization of the latter. We conclude that symbolic decision procedures may meet requirements for assisting human operators in hazardous situations more satisfactorily than classical decision procedures.

scholarly journals Reasoning with Triggers

10.29007/3c1n ◽  
2018 ◽  
Author(s):  
Claire Dross ◽  
Sylvain Conchon ◽  
Johannes Kanig ◽  
Andrei Paskevich
Keyword(s):  
Decision Procedure ◽  
Decision Procedures ◽  
Description Language ◽  
Smt Solver ◽  
First Order ◽  
Smt Solvers ◽  
Precise Sense ◽  
Universal Quantifiers ◽  
Internal Knowledge

SMT solvers can decide the satisfiability of ground formulas modulo a combination ofbuilt-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures.In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of first-order axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate using the theory of arrays, how such proofs can be achieved in our formalism.

scholarly journals Effectively Monadic Predicates

10.29007/drll ◽  
2018 ◽  
Author(s):  
Margus Veanes ◽  
Nikolaj Bjorner ◽  
Lev Nachmanson ◽  
Sergey Bereg
Keyword(s):  
Decision Procedure ◽  
Decision Procedures ◽  
Boolean Combination ◽  
Background Theory ◽  
Symbolic Automata

Monadic predicates play a prominent role in many decidable cases, including decision procedures for symbolic automata. We are here interested in discovering whether a formula can be rewritten into a Boolean combination of monadic predicates. Our setting is quantifier-free formulas over a decidable background theory, such as arithmetic and we here develop a semi-decision procedure for extracting a monadic decomposition of a formula when it exists.

Decision Support for Psychiatric Diagnosis Based on a Simple Questionnaire

1997 ◽  
Vol 36 (04/05) ◽  
pp. 349-351
Author(s):  
H. Mizuta ◽  
K. Kawachi ◽  
H. Yoshida ◽  
K. Iida ◽  
Y. Okubo ◽  
...  
Keyword(s):  
Neural Network ◽  
Decision Support ◽  
Psychiatric Diagnosis ◽  
Psychiatric Patients ◽  
Bayesian Classifier ◽  
Neural Network Classifier ◽  
Correct Decision ◽  
Neurotic Disorders ◽  
The Neural Network

Abstract:This paper compares two classifiers: Pseudo Bayesian and Neural Network for assisting in making diagnoses of psychiatric patients based on a simple yes/no questionnaire which is provided at the outpatient’s first visit to the hospital. The classifiers categorize patients into three most commonly seen ICD classes, i.e. schizophrenic, emotional and neurotic disorders. One hundred completed questionnaires were utilized for constructing and evaluating the classifiers. Average correct decision rates were 73.3% for the Pseudo Bayesian Classifier and 77.3% for the Neural Network classifier. These rates were higher than the rate which an experienced psychiatrist achieved based on the same restricted data as the classifiers utilized. These classifiers may be effectively utilized for assisting psychiatrists in making their final diagnoses.

Sign in / Sign up

Export Citation Format

Share Document