اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدLogical Primes, Metavariables and Satisfiability
81
0
0.0
(
0
)
تأليف
Bernd R. Schuh
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
For formulas F of propositional calculus I introduce a metavariable MF and show how it can be used to define an algorithm for testing satisfiability. MF is a formula which is true/false under all possible truth assignments iff F is satisfiable/unsatisfiable. In this sense MF is a metavariable with the meaning F is SAT. For constructing MF a group of transformations of the basic variables ai is used which corresponds to flipping literals to their negation. The whole procedure corresponds to branching algorithms where a formula is split with respect to the truth values of its variables, one by one. Each branching step corresponds to an approximation to the metatheorem which doubles the chance to find a satisfying truth assignment but also doubles the length of the formulas to be tested, in principle. Simplifications arise by additional length reductions. I also discuss the notion of logical primes and show that each formula can be written as a uniquely defined product of such prime factors. Satisfying truth assignments can be found by determining the missing primes in the factorization of a formula.
قيم البحث
اقرأ أيضاً
We consider the operation of sum on Kripke frames, where a family of frames-summands is indexed by elements of another frame. In many cases, the modal logic of sums inherits the finite model property and decidability from the modal logic of summands.
In this paper we show that, under a general condition, the satisfiability problem on sums is polynomial space Turing reducible to the satisfiability problem on summands. In particular, for many modal logics decidability in PSPACE is an immediate corollary from the semantic characterization of the logic.
The development of compositional distributional models of semantics reconciling the empirical aspects of distributional semantics with the compositional aspects of formal semantics is a popular topic in the contemporary literature. This paper seeks t
o bring this reconciliation one step further by showing how the mathematical constructs commonly used in compositional distributional models, such as tensors and matrices, can be used to simulate different aspects of predicate logic. This paper discusses how the canonical isomorphism between tensors and multilinear maps can be exploited to simulate a full-blown quantifier-free predicate calculus using tensors. It provides tensor interpretations of the set of logical connectives required to model propositional calculi. It suggests a variant of these tensor calculi capable of modelling quantifiers, using few non-linear operations. It finally discusses the relation between these variants, and how this relation should constitute the subject of future work.
This note introduces a generalization to the setting of infinite-time computation of the busy beaver problem from classical computability theory, and proves some results concerning the growth rate of an associated function. In our view, these results
indicate that the generalization is both natural and promising.
The constraint satisfaction problem (CSP) of a first-order theory $T$ is the computational problem of deciding whether a given conjunction of atomic formulas is satisfiable in some model of $T$. We study the computational complexity of $mathrm{CSP}(T
_1 cup T_2)$ where $T_1$ and $T_2$ are theories with disjoint finite relational signatures. We prove that if $T_1$ and $T_2$ are the theories of temporal structures, i.e., structures where all relations have a first-order definition in $(mathbb{Q};<)$, then $mathrm{CSP}(T_1 cup T_2)$ is in P or NP-complete. To this end we prove a purely algebraic statement about the structure of the lattice of locally closed clones over the domain ${mathbb Q}$ that contain $mathrm{Aut}(mathbb{Q};<)$.
Robin Hirsch posed in 1996 the Really Big Complexity Problem: classify the computational complexity of the network satisfaction problem for all finite relation algebras $bf A$. We provide a complete classification for the case that $bf A$ is symmetri
c and has a flexible atom; the problem is in this case NP-complete or in P. If a finite integral relation algebra has a flexible atom, then it has a normal representation $mathfrak{B}$. We can then study the computational complexity of the network satisfaction problem of ${bf A}$ using the universal-algebraic approach, via an analysis of the polymorphisms of $mathfrak{B}$. We also use a Ramsey-type result of Nev{s}etv{r}il and Rodl and a complexity dichotomy result of Bulatov for conservative finite-domain constraint satisfaction problems.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
