A machine program for theorem-proving

DOI10.1145/368273.368557zbMATH Open0217.54002DBLPjournals/cacm/DavisLL62OpenAlexW2057361103WikidataQ29399031 ScholiaQ29399031MaRDI QIDQ5621961FDOQ5621961

Authors: George Logemann, Donald W. Loveland, Martin Davis 

Publication date: 1962

Published in: Communications of the ACM (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2027/mdp.39015095248095

Recommendations

• A theorem prover for a computational logic
• Publication:3490989
• scientific article; zbMATH DE number 1360950
• scientific article; zbMATH DE number 13446
• scientific article; zbMATH DE number 4155933
• Mechanical proofs about computer programs
• Proofs as programs
• scientific article; zbMATH DE number 432701
• Computer theorem proving in mathematics

Mathematics Subject Classification ID

Cited In (only showing first 100 items - show all)

• Symmetric matroid polytopes and their generation
• Editorial: Symbolic computation and satisfiability checking
• Formally verifying the solution to the Boolean Pythagorean triples problem
• Learning to select branching rules in the DPLL procedure for satisfiability
• Generating hard satisfiability problems
• Challenges in Constraint-Based Analysis of Hybrid Systems
• New upper bound for the \#3-SAT problem
• Symbolic techniques in satisfiability solving
• Fast congruence closure and extensions
• Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic
• New methods for proving the impossibility to solve problems through reduction of problem spaces
• Conformant planning as a case study of incremental QBF solving
• An efficient approach to solving random \(k\)-SAT problems
• John McCarthy's legacy
• Engineering constraint solvers for automatic analysis of probabilistic hybrid automata
• A competitive and cooperative approach to propositional satisfiability
• Substitutions into propositional tautologies
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Craig interpolation in the presence of non-linear constraints
• A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
• Propositional SAT solving
• Density condensation of Boolean formulas
• Heuristic-based backtracking relaxation for propositional satisfiability
• Solving non-Boolean satisfiability problems with stochastic local search: A comparison of encodings
• The SAT-based approach to separation logic
• The complexity of pure literal elimination
• Regular and General Resolution: An Improved Separation
• Toward unification of exact and heuristic optimization methods
• Complete on average Boolean satisfiability
• An empirical study of constraint logic programming and answer set programming solutions of combinatorial problems
• Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances
• A weight-balanced branching rule for SAT
• New complexity results for Łukasiewicz logic
• The complexity of resolution refinements
• A two-phase algorithm for solving a class of hard satisfiability problems
• A logical approach to efficient Max-SAT solving
• Rigorous results for random (\(2+p)\)-SAT
• Results related to threshold phenomena research in satisfiability: Lower bounds
• Short propositional refutations for dense random 3CNF formulas
• A unified framework for DPLL(T) + certificates
• Unrestricted vs restricted cut in a tableau method for Boolean circuits
• A SAT-based parser and completer for pictures specified by tiling
• A Groebner bases-based approach to backward reasoning in rule based expert systems
• How good are branching rules in DPLL?
• A Bayesian approach to tackling hard computational problems. (Preliminary report)
• Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT
• Foundations of \(r\)-contiguous matching in negative selection for anomaly detection
• Configuration landscape analysis and backbone guided local search. I: Satisfiability and maximum satisfiability
• The mechanical verification of a DPLL-based satisfiability solver
• A Unified Framework for Certificate and Compilation for QBF
• Average time analyses of simplified Davis-Putnam procedures
• Improved algorithms for the general exact satisfiability problem
• Solving SAT by algorithm transform of Wu's method
• SAT-solving in practice, with a tutorial example from supervisory control
• A parallel approach for theorem proving in propositional logic
• A sharp threshold in proof complexity yields lower bounds for satisfiability search
• Leveraging belief propagation, backtrack search, and statistics for model counting
• Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K
• Formal verification of a generic framework to synthesize SAT-provers
• A search-based procedure for nonlinear real arithmetic
• Backjumping for quantified Boolean logic satisfiability
• On market-inspired approaches to propositional satisfiability
• Algorithms for Solving Satisfiability Problems with Qualitative Preferences
• Interpolant learning and reuse in SAT-based model checking
• Matroid enumeration for incidence geometry
• Conflict-directed \(A^{*}\) and its role in model-based embedded systems
• New methods for 3-SAT decision and worst-case analysis
• Conformant planning via heuristic forward search: A new approach
• Generalised graph colouring by a hybrid of local search and constraint programming
• MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability
• GridSAT: Design and implementation of a computational grid application
• The state of SAT
• Solving satisfiability problems with preferences
• BerkMin: A fast and robust SAT-solver
• Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions
• On the structure of some classes of minimal unsatisfiable formulas
• SatEx: A web-based framework for SAT experimentation
• Multi-threaded ASP solving with clasp
• First order Stålmarck. Universal lemmas through branch merges
• Limitations of restricted branching in clause learning
• The Relative Power of Semantics and Unification
• MaxMinMax problem and sparse equations over finite fields
• Treewidth computation and extremal combinatorics
• Exploiting the real power of unit propagation lookahead
• Curriculum-based course timetabling with SAT and MaxSAT
• Relating constraint answer set programming languages and algorithms
• Parameterized complexity of DPLL search procedures
• SATO: An efficient propositional prover
• Interpolation systems for ground proofs in automated deduction: a survey
• An experiment with satisfiability modulo SAT
• Semantically-guided goal-sensitive reasoning: model representation
• Experimental results on the crossover point in random 3-SAT
• Explaining the \texttt{cumulative} propagator
• A self-adaptive multi-engine solver for quantified Boolean formulas
• On deciding satisfiability by theorem proving with speculative inferences
• Extending and implementing the stable model semantics
• Deciding floating-point logic with abstract conflict driven clause learning
• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• Stochastic enumeration method for counting NP-hard problems
• Answer set programming based on propositional satisfiability

Uses Software

• tawSolver

This page was built for publication: A machine program for theorem-proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5621961)