The Boolean Solution Problem from the Perspective of Predicate Logic - Extended Version
Finding solution values for unknowns in Boolean equations was a principal reasoning mode in the Algebra of Logic of the 19th century. Schr\"oder investigated it as "Aufl\"osungsproblem" ("solution problem"). It is closely related to the modern notion of Boolean unification. Today it is commonly presented in an algebraic setting, but seems potentially useful also in knowledge representation based on predicate logic. We show that it can be modeled on the basis of first-order logic extended by second-order quantification. A wealth of classical results transfers, foundations for algorithms unfold, and connections with second-order quantifier elimination and Craig interpolation show up. Although for first-order inputs the set of solutions is recursively enumerable, the development of constructive methods remains a challenge. We identify some cases that allow constructions, most of them based on Craig interpolation, and show a method to take vocabulary restrictions on solution components into account.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Graph Neural Reasoning May Fail in Certifying Boolean Unsatisfiability
It is feasible and practically-valuable to bridge the characteristics between graph neural networks (GNNs) and logical reasoning. Despite considerable efforts and successes witnessed to solve Boolean satisfiability (SAT)…
Logical ReasoningGraph Neural Networks for Reasoning 2-Quantified Boolean Formulas
It is valuable yet remains challenging to apply neural networks in logical reasoning tasks. Despite some successes witnessed in learning SAT (Boolean Satisfiability) solvers for propositional logic via Graph Neural Netwo…
Logical ReasoningLearning Algorithms via Neural Logic Networks
We propose a novel learning paradigm for Deep Neural Networks (DNN) by using Boolean logic algebra. We first present the basic differentiable operators of a Boolean system such as conjunction, disjunction and exclusive-O…
Inductive logic programmingSymmetry Breaking Predicates for SAT-based DFA Identification
It was shown before that the NP-hard problem of deterministic finite automata (DFA) identification can be effectively translated to Boolean satisfiability (SAT). Modern SAT-solvers can tackle hard DFA identification inst…
Risk-Bounded Temporal Logic Control of Continuous-Time Stochastic Systems
Motivated by the recent interest in risk-aware control, we study a continuous-time control synthesis problem to bound the risk that a stochastic linear system violates a given specification. We use risk signal temporal l…