Solvable cases of the decision problem
From MaRDI portal
Publication:2651970
zbMath0056.24505MaRDI QIDQ2651970
Publication date: 1954
Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)
Related Items (81)
Turing-machines and the Entscheidungsproblem ⋮ Towards automating duality ⋮ Logical equations in monadic logic ⋮ Satisfiability Modulo Theories ⋮ Efficient ground completion ⋮ The equational theory of union-free algebras of relations ⋮ Model theory of monadic predicate logic with the infinity quantifier ⋮ Decidability and incompleteness results for first-order temporal logics of linear time ⋮ Controlled query evaluation with open queries for a decidable relational submodel ⋮ Generalizing DPLL and satisfiability for equalities ⋮ Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ Implication of clauses is undecidable ⋮ The Cut Elimination Theorem in the Unary Second Order Language ⋮ Set Constraints, Pattern Match Analysis, and SMT ⋮ Formal verification of synchronous data-flow program transformations toward certified compilers ⋮ On the completeness and the decidability of strictly monadic second‐order logic ⋮ On an automated translation of modal proof rules into formulas of the classical logic ⋮ The modal logic of inequality ⋮ Complexity, convexity and combinations of theories ⋮ MAXIMALITY OF LOGIC WITHOUT IDENTITY ⋮ Solvable classes of pseudoprenex formulas ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Verifying Heap-Manipulating Programs in an SMT Framework ⋮ Discrete dualities for \(n\)-potent MTL-algebras and 2-potent BL-algebras ⋮ Quantifiers as modal operators ⋮ INTERLEAVING LOGIC AND COUNTING ⋮ Efficient theory combination via Boolean search ⋮ NuMDG: a new tool for multiway decision graphs construction ⋮ Complexity results for classes of quantificational formulas ⋮ Elementary intuitionistic theories ⋮ The finite controllability of the Maslov case ⋮ The decision problem for database dependencies ⋮ Unnamed Item ⋮ Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. ⋮ Embedding relations in the lattice of recursively enumerable sets ⋮ Resolution proof transformation for compression and interpolation ⋮ Solving constraint satisfaction problems with SAT modulo theories ⋮ Discriminator varieties and symbolic computation ⋮ Zur Theorie Der Spektralen Darstellung Von Prädikaten Durch Ausdrücke Der Prädikatenlogik 1. Stufe ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Inferring the equivalence of functional programs that mutate data ⋮ A method for simultaneous search for refutations and models by equational constraint solving ⋮ The Strategy Challenge in SMT Solving ⋮ Transforming equality logic to propositional logic ⋮ The existential graphs ⋮ Relational completeness of query languages for annotated databases ⋮ A Term Rewriting Technique for Decision Graphs ⋮ Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols ⋮ In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs ⋮ A randomized satisfiability procedure for arithmetic and uninterpreted function symbols ⋮ Program schemata and the first-order decision problem ⋮ Building small equality graphs for deciding equality logic with uninterpreted functions ⋮ On reasoning about structural equality in XML: a description logic approach ⋮ The characterization of monadic logic ⋮ Zero, successor and equality in BDDs ⋮ The polynomial-time hierarchy ⋮ Embedded software verification using symbolic execution and uninterpreted functions ⋮ HEINRICH BEHMANN’S 1921 LECTURE ON THE DECISION PROBLEM AND THE ALGEBRA OF LOGIC ⋮ Address at the Princeton University Bicentennial Conference on Problems of Mathematics (December 17–19, 1946), By Alfred Tarski ⋮ Program transformations and algebraic semantics ⋮ Order-Sorted Rewriting and Congruence Closure ⋮ Set constraints in some equational theories ⋮ A completion procedure for conditional equations ⋮ The decision problem for the logic of predicates and of operations ⋮ EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas ⋮ Mechanical theorem proving in a certain class of formulae of the predicate calculus ⋮ On the Gödel class with identity ⋮ A strong version of Herbrand's theorem for introvert sentences ⋮ A New Approach for the Construction of Multiway Decision Graphs ⋮ SGGS decision procedures ⋮ The small model property: How small can it be? ⋮ Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic ⋮ Model-based Theory Combination ⋮ Generalized quantifiers and modal logic ⋮ Thue trees ⋮ SET-VAR ⋮ La théorie des fonctions récursives et ses applications. (Exposé d'information générale) ⋮ Interpolation for first order S5 ⋮ The unsolvability of the Gödel class with identity ⋮ Representability in second-order propositional poly-modal logic
This page was built for publication: Solvable cases of the decision problem
