1,720,994 research outputs found
Applying the Davis-Putnam procedure to non-clausal formulas
No full textTraditionally, the satisfiability problem for propositional logics deals with formulas in Conjunctive Normal Form (CNF). A typical way to deal with non-CNF formulas requires (i) converting them into CNF, and (ii) applying solvers usually based on the Davis-Putnam (DP) procedure. A well known problem of this solution is that the CNF conversion may introduce many new variables, thus greatly widening the space of assignments in which the DP procedure has to search in order to find solutions.
In this paper we present two variants of the DP procedure which overcome the problem outlined above. The idea underlying these variants is that splitting should occur only for the variables in the original formula. The CNF conversion methods employed ensure their correctness and completeness. As a consequence, we get two decision procedures for non-CNF formulas (i) which can exploit all the present and future sophisticated technology of current DP implementations, and (ii) whose space of assignments they have to search in, is limited in size by the number of variables in the original input formula.
The preliminary analysis reported in [14] shows that these ideas can lead to a significant speed up of the search procedur
Ideal and Real Belief about Belief: Some Intuitions
No full textIt is widely recognized that intelligent and autonomous agents operating in a distributed environment must be able to reason about their own and other agents` beliefs. Standard possible world semantics, usually used for such an endeavor, lead to formalization in which agents suffer the ‘logical omniscience problem’ – thy believe all valid formulas and all the logical consequences of their own beliefs. As far as we know, no taxonomic analysis exists which describes all the possible ways in which this phenomenon can or can not arise. The goal of this paper is to fill this gap. Our approach is based on the idea of first providing a set-theoretic specification of agents’ beliefs, and then to define constructors for such sets. This allow us first to provide a set of constructors can be modified to generate real believers. The constructors defined turn out to be inference rules inside a multicontext syste
Ideal and Real Belief about Belief
No full textThe goal of this paper is to provide a taxonomic characterization of the possible forms of belief about belief. Our analysis is performed in two steps. First, we give a set-theoretic specification of beliefs about beliefs, i.e. we characterize them as particular sets satisfying certain closure conditions. Second, we define a set of constructors which generate all and only the objects belonging to these sets. The constructors defined turn out to be inference rules inside a multicontext system. We provide some intuitions about the expressive power and conceptual importance of the multicontext systems defined by proving and discussing some equivalence results with some important modal system
Act, and the Rest Will Follow: Exploiting Determinism in Planning as Satisfiability
No full textIn this paper we focus on Planning as Satisfiability (SAT). We build from the simple consideration that the values of fluents at a certain time point derive deterministically from the initial situation and the sequence of actions performed till that point. Thus, the choice of actions to perform is the only source of nondeterminism. This is a rather trivial considerations, but which has important positive consequences if implemented in current planners via SAT. In fact, it produces a dramatic size reduction of the space of the truth assignments searched in by the SAT decider used to solve the final SAT problem. To justify this claim, we repeat many of the experiments reported in (Erns, Millstein, & Weld 1997), and show that the CPU time requested to solve a problem can go down up to 4 orders of magnitud
*SAT, KsatC, DLP and TA: a comparative analysis
No full textWe comparatively test *SAT (our latest system for testing the satisfiability of a formula in the modal logic K or in the description logic ALC) with other state-of-the-art systems on a set of randomly generated tests. The experimental analysis shows that on these tests *SAT performs better than or as well as the other system
SAT-Based Decision Procedures for Classical Modal Logics
Full text linkWe present a set of SAT-based decision procedures for various classical modal logics. By SAT-based, we mean built on top of a SAT solver. We show how the SAT-based approach allows for a modular implementation for these logics. For some of the logics we deal with, we are not aware of any other implementation. For the others, we define a testing methodology which generalizes the 3CNFK methodology by Giunchiglia and Sebastiani. The experimental evaluation shows that our decision procedures perform better than or as well as other state-of-the-art decision procedures
SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation
No full textThis paper follows on previous papers which present and evaluate various decision procedures for modal logics. It confirms previous experimental results in showing that SAT based decision procedures, i.e., the procedures built on top of decision procedures for propositional satisfiability, are more efficient than tableau based decision procedures. It also confirms previous evidence of an easy-hard-easy pattern in the satisfiability curve for modal K. Finally, it provides further experimental results, suggesting that SAT based decision procedures are also more efficient than the decision procedures based on translation methods. These results contradict some of the claims presented in previous papers by other author
Dealing with Expected and Unexpected Obstacles
No full textThe goal of this paper is to show how contexts can be used together with circumscription to provide a general solution to the qualification problem. The context mechanism is used to perform theory refomulation before performing non monotonic reasoning (i
- …
