Despite being fairly powerful, finite non-deterministic matrices are unable to characterize some logics of formal inconsistency, such as those found between mbCcl and Cila. In order to overcome this limitation, we propose here restricted non-deterministic matrices (in short, RNmatrices), which are non-deterministic algebras together with a subset of the set of valuations. This allows us to characterize not only mbCcl and Cila (which is equivalent, up to language, to da Costa's logic C_1) but the whole hierarchy of da Costa's calculi (...) C_n. This produces a novel decision procedure for these logics. Moreover, we show that the RNmatrix semantics proposed here induces naturally a labelled tableau system for each C_n, which constitutes another decision procedure for these logics. This new semantics allows us to conceive da Costa's hierarchy of C-systems as a family of (non deterministically) (n+2)-valued logics, where n is the number of "inconsistently true" truth-values and 2 is the number of "classical" or "consistent" truth-values, for every C_n. (shrink)

A system of natural deduction is presented whose set of theses is identical with that of the systemE of entailment. For that system a decision procedure is described proving the decidability ofE.

I argue that the Universal Law formulation of the Categorical Imperative is best interpreted as a test or decision procedure of moral rightness and not as a criterion intended to explain the deontic status of actions. Rather, the Humanity formulation is best interpreted as a moral criterion. I also argue that because the role of a moral criterion is to explain, and thus specify what makes an action right or wrong, Kant's Humanity formulation yields a theory of relevant (...) descriptions. (shrink)

I argue that partialist critics of deontological theories make a mistake similar to one made by critics of utilitarianism: they fail to distinguish between a theory’s decision procedure and its standard of rightness. That is, they take these deontological theories to be offering a method for moral deliberation when they are in fact offering justificatory arguments for moral principles. And while deontologists, like utilitarians do incorporate impartiality into their justifications for basic principles, many do not require that agents (...) utilize impartial methods of moral deliberation. It follows that insofar as partialists reject impartiality in deliberation, their criticisms may miss their mark. If however, partialists are opposed to justifications for basic principles that rely upon impartiality, they are committed, I argue, to drastic revisions in moral theory that have worrisome implications. (shrink)

This paper describes a decision procedure for disjunctions of conjunctions of anti-prenex normal forms of pure first-order logic (FOLDNFs) that do not contain V within the scope of quantifiers. The disjuncts of these FOLDNFs are equivalent to prenex normal forms whose quantifier-free parts are conjunctions of atomic and negated atomic formulae (= Herbrand formulae). In contrast to the usual algorithms for Herbrand formulae, neither skolemization nor unification algorithms with function symbols are applied. Instead, a procedure is described (...) that rests on nothing but equivalence transformations within pure first-order logic (FOL). This procedure involves the application of a calculus for negative normal forms (the NNF-calculus) with A -||- A & A (= &I) as the sole rule that increases the complexity of given FOLDNFs. The described algorithm illustrates how, in the case of Herbrand formulae, decision problems can be solved through a systematic search for proofs that reduce the number of applications of the rule &I to a minimum in the NNF-calculus. In the case of Herbrand formulae, it is even possible to entirely abstain from applying &I. Finally, it is shown how the described procedure can be used within an optimized general search for proofs of contradiction and what kind of questions arise for a &I-minimal proof strategy in the case of a general search for proofs of contradiction. (shrink)

Let F be the set of functions from an infinite set, S, to an ordered ring, R.

This paper proves decidability of a range of weak relevant logics using decision procedures based on the Routley-Meyer semantics. Logics are categorized as F-logics, for those proved decidable using a filtration method, and U-logics, for those proved decidable using a direct (unfiltered) method. Both of these methods are set out as reductio methods, in the style of Hughes and Cresswell. We also examine some extensions of the U-logics where the method fails and infinite sequences of worlds can be generated.

In this paper, I present a decision procedure for evaluating arguments expressed in natural language. I think that other instructors of informal logic and critical thinking might find this decision procedure to be a useful addition to their teaching resources.

We consider several natural fragments of the alternating-time temporal logics ATL* and ATL with restrictions on the nesting between temporal operators and strategic quantifiers. We develop optimal decision procedures for satisfiability in these fragments, showing that they have much lower complexities than the full languages. In particular, we prove that the satisfiability problem for state formulae in the full `strategically flat' fragment of ATL* is PSPACE-complete, whereas the satisfiability problems in the flat fragments of ATL and ATL$^{+}$ are $\Sigma^P_3$-complete. (...) We note that the nesting hierarchies for fragments of ATL* collapse in terms of expressiveness above nesting depth 1, hence our results cover all such fragments with lower complexities. (shrink)

(new version: 10/30/07). Click here to download the companion Mathematica 6 notebook that goes along with this paper.

In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to some 1-degree formula, i.e. a modally-flat formula with modal functors having only boolean formulas in its scope. In contrast to many sequent calculi for S5 the presented system does not introduce any extra devices. Thus it is a standard version of (...) SC but with some additional simple rewrite rules. The procedure combines the proces of saturation of sequents with reduction of their elements to some normal modal form. (shrink)

Some investigations into the algebraic constructive aspects of a decision procedure for various fragments of Relevant Logics are presented. Decidability of these fragments relies on S. Kripke's gentzenizations and on his combinatorial lemma known as Kripke's lemma that B. Meyer has shown equivalent to Dickson's lemma in number theory and to his own infinite divisor lemma, henceforth, Meyer's lemma or IDP. These investigations of the constructive aspects of the Kripke's-Meyer's decision procedure originate in the development of (...) Paul Thistlewaite's “Kripke” theorem prover that had been devised to tackle the decision problem of the Relevant Logic R. A. Urquhart's pen and paper solution that relies on a sophisticated algebraic and geometric treatment of the problem shows the usefulness of an algebraic approach in Logic. Here, the study of the constructive aspects of the Kripke-Meyer decision procedure relies on various algebraic constructive results in the theory of polynomials rings. (shrink)

Hybrid logics are extensions of standard modal logics, which significantly increase the expressive power of the latter. Since most of hybrid logics are known to be decidable, decision procedures for them is a widely investigated field of research. So far, several tableau calculi for hybrid logics have been presented in the literature. In this paper we introduce a sound, complete and terminating tableau calculus T H(@,E,D, ♦ −) for hybrid logics with the satisfaction operators, the universal modality, the difference (...) modality and the inverse modality as well as the corresponding sequent calculus S H(@,E,D, ♦ −) . They not only uniformly cover relatively wide range of various hybrid logics but they are also conceptually simple and enable effective search for a minimal model for a satisfiable formula. The main novelty is the exploitation of the unrestricted blocking mechanism introduced as an explicit, sound tableau rule. (shrink)

We introduce the notion of “δ-complete decision procedures” for solving SMT problems over the real numbers, with the aim of handling a wide range of nonlinear functions including transcendental functions and solutions of Lipschitz-continuous ODEs. Given an SMT problemϕ and a positive rational number δ, a δ-complete decision procedure determines either that ϕ is unsatisfiable, or that the “δ-weakening” of ϕ is satisfiable. Here, the δ-weakening of ϕ is a variant of ϕ that allows δ-bounded numerical perturbations (...) on ϕ. We establish the existence and complexity of δ-complete decision procedures for bounded SMT over reals with functions mentioned above. We propose to use δ-completeness as an ideal requirement for numerically-driven decision procedures. As a concrete example, we formally analyze the DPLL〈ICP〉 framework, which integrates Interval Constraint Propagation in DPLL, and establish necessary and sufficient conditions for its δ-completeness. We discuss practical applications of δ-complete decision procedures for correctness-critical applications including formal verification and theorem proving. (shrink)

We address the general problem of determining the validity of boolean combinations of equalities and inequalities between real-valued expressions. In particular, we consider methods of establishing such assertions using only restricted forms of distributivity. At the same time, we explore ways in which “local'’ decision or heuristic procedures for fragments of the theory of the reals can be amalgamated into global ones. Let $Tadd[QQ]$ be the first-order theory of the real numbers in the language with symbols $0, 1, +, (...) -. (shrink)

We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi\-agent epistemic logic \CMAELCD\ with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for \CMAELCD\ and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using that result, we design an incremental tableau-building procedure that eventually constructs a satisfying Hintikka structure for every satisfiable (...) input set of formulae of \CMAELCD\ and closes for every unsatisfiable input set of formulae. (shrink)

In Section 2 I give a criterion of decidability that can be applied to logics (i.e. Tarski consequence operators) without the finite model property. In Section 3 I study ukasiewicz-style refutation procedures as a method of obtaining decidability results.This method also proves to be more general than Harrop's criterion.

We focus on two formal methods contexts which generate investigations into decision problems for finite strings.

D. A. Lloyd Thomas; VIII—Political Decision Procedures1, Proceedings of the Aristotelian Society, Volume 70, Issue 1, 1 June 1970, Pages 141–160, https://doi.or.

A class of many-sorted polyadic set algebras is introduced. These generalise structure and model in a way that is relevant in regards to the Entscheidungsproblem and to automated reasoning.A downward Löwenheim-Skolem property is shown in that each satisfiable finite conjunction of purely relational first-order prenex sentences has a finite generalised model. This property does, together with a construction related to doubling the size of a finite structure, provide several strict generalisations of the strategy of finite model search for disproving.

Moral decision procedures such as principlism or casuistry require intuition at certain junctures, as when a principle seems indeterminate, or principles conflict, or we wonder which paradigm case is most relevantly similar to the instant case. However, intuitions are widely thought to lack epistemic justification, and many ethicists urge that such decision procedures dispense with intuition in favor of forms of reasoning that provide discursive justification. I argue that discursive justification does not eliminate or minimize the need for (...) intuition, or constrain our intuitions. However, this is not a problem, for intuitions can be justified in easy or obvious cases, and decision procedures should be understood as heuristic devices for reaching judgments about harder cases that approximate the justified intuitions we would have about cases under ideal conditions, where hard cases become easy. Similarly, the forms of reasoning which provide discursive justification help decision procedures perform this heuristic function not by avoiding intuition, but by making such heuristics more accurate. Nonetheless, it is possible to demand too much justification; many clinical ethicists lack the time and philosophical training to reach the more elaborate levels of discursive justification. We should keep moral decision procedures simple and user-friendly so that they will provide what justification can be achieved under clinical conditions, rather than trying to maximize our epistemic justification out of an overstated concern about intuition. (shrink)

A standard objection to act utilitarian theories is that they are not helpful in deciding what it is morally permissible for us to do when we actually have to make a choice between alternatives. That is, such theories are worthless as decision procedures. A standard reply to this objection is that act utilitarian theories can be evaluated solely as theories about right-making characteristics and, when so evaluated, their inadequacy as decision procedures is irrelevant. Even if somewhat unappealing, this (...) is an effective reply to the standard objection. (shrink)

One semantic and two syntactic decision procedures are given for determining the validity of Aristotelian assertoric and apodeictic syllogisms. Results are obtained by using the Aristotelian deductions that necessarily have an even number of premises.

We present a dual tableau system, RLK, which is itself a deterministic decision procedure verifying validity of K-formulas. The system is constructed in the framework of the original methodology of relational proof systems, determined only by axioms and inference rules, without any external techniques. Furthermore, we describe an implementation of the system RLK in Prolog, and we show some of its advantages.

We present a dual tableau system, RLK, which is itself a deterministic decision procedure verifying validity of K-formulas. The system is constructed in the framework of the original methodology of relational proof systems, determined only by axioms and inference rules, without any external techniques. Furthermore, we describe an implementation of the system in Prolog, and we show some of its advantages.