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.

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 Symbolic WS1S

10.29007/t28j ◽  
2018 ◽  
Author(s):  
Loris D'Antoni ◽  
Margus Veanes
Keyword(s):  
Blow Up ◽  
Finite Automata ◽  
Decision Procedures ◽  
Second Order ◽  
Order Logic ◽  
Symbolic Logic ◽  
First Order ◽  
Symbolic Automata ◽  
Second Order Logic ◽  
Monadic Second Order Logic

We extend weak monadic second-order logic of one successor (WS1S) to symbolic alphabets byallowing character predicates to range over decidable first order theories and not just finite alphabets.We call this extension symbolic WS1S (s-WS1S). We then propose two decision procedures for such alogic: 1) we use symbolic automata to extend the classic reduction from WS1S to finite automata toour symbolic logic setting; 2) we show that every s-WS1S formula can be reduced to a WS1S formulathat preserves satisfiability, at the price of an exponential blow-up.

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.

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.

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 Chapter 33. Satisfiability Modulo Theories

2021 ◽  
Author(s):  
Clark Barrett ◽  
Roberto Sebastiani ◽  
Sanjit A. Seshia ◽  
Cesare Tinelli
Keyword(s):  
Relevant Literature ◽  
Finite Size ◽  
Decision Procedures ◽  
Research Field ◽  
Satisfiability Modulo Theories ◽  
Practical Applications ◽  
First Order ◽  
Background Theory ◽  
Sat Solver ◽  
And Function

Applications in artificial intelligence, formal verification, and other areas have greatly benefited from the recent advances in SAT. It is often the case, however, that applications in these fields require determining the satisfiability of formulas in more expressive logics such as first-order logic. Also, these applications typically require not general first-order satisfiability, but rather satisfiability with respect to some background theory, which fixes the interpretations of certain predicate and function symbols. For many background theories, specialized methods yield decision procedures for the satisfiability of quantifier-free formulas or some subclass thereof. Specialized decision procedures have been discovered for a long and still growing list of theories with practical applications. These include the theory of equality, various theories of arithmetic, and certain theories of arrays, as well as theories of lists, tuples, records, and bit-vectors of a fixed or arbitrary finite size. The research field concerned with determining the satisfiability of formulas with respect to some background theory is called Satisfiability Modulo Theories (SMT). This chapter provides a brief overview of SMT together with references to the relevant literature for a deeper study. It begins with an overview of techniques for solving SMT problems by encodings to SAT. The rest of the chapter is mostly concerned with an alternative approach in which a SAT solver is integrated with a separate decision procedure (called a theory solver) for conjunctions of literals in the background theory. After presenting this approach as a whole, the chapter provides more details on how to construct and combine theory solvers, and discusses several extensions and enhancements.

Sign in / Sign up

Export Citation Format

Share Document