A machine program for theorem-proving
From MaRDI portal
Recommendations
- A theorem prover for a computational logic
- scientific article; zbMATH DE number 4164171
- 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
Cited in
(only showing first 100 items - show all)- A generative power-law search tree model
- A self-adaptive multi-engine solver for quantified Boolean formulas
- An approach for extracting a small unsatisfiable core
- A rigorous methodology for specification and verification of business processes
- Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
- \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver
- Data compression for proof replay
- First order Stålmarck. Universal lemmas through branch merges
- Theory decision by decomposition
- Symmetric matroid polytopes and their generation
- A parallel approach for theorem proving in propositional logic
- An exponential lower bound for the pure literal rule
- How good are branching rules in DPLL?
- Length of prime implicants and number of solutions of random CNF formulae
- A two-phase algorithm for solving a class of hard satisfiability problems
- An average case analysis of a resolution principle algorithm in mechanical theorem proving.
- A BDD SAT solver for satisfiability testing: An industrial case study
- Reconstructing (h,v)-convex 2-dimensional patterns of objects from approximate horizontal and vertical projections.
- Approximating minimal unsatisfiable subformulae by means of adaptive core search
- How to fake an RSA signature by encoding modular root finding as a SAT problem
- Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT.
- Resolution and binary decision diagrams cannot simulate each other polynomially
- Worst-case study of local search for MAX-\(k\)-SAT.
- On the structure of some classes of minimal unsatisfiable formulas
- Equivalent literal propagation in the DLL procedure
- On the limit of branching rules for hard random unsatisfiable 3-SAT
- A satisfiability procedure for quantified Boolean formulae
- SAT problems with chains of dependent variables
- Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
- Equivalency reasoning to solve a class of hard SAT problems.
- Extending and implementing the stable model semantics
- Backjump-based backtracking for constraint satisfaction problems
- Proving unsatisfiability of CNFs locally
- Nagging: A scalable fault-tolerant paradigm for distributed search
- A note about k-DNF resolution
- P\(_-\)UNSAT approach of attractor calculation for Boolean gene regulatory networks
- Satisfiability modulo theory (SMT) formulation for optimal scheduling of task graphs with communication delay
- Relating size and width in variants of Q-resolution
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Three-valued semantics for hybrid MKNF knowledge bases revisited
- Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms
- Efficient, verified checking of propositional proofs
- What is answer set programming to propositional satisfiability
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Cliques enumeration and tree-like resolution proofs
- Mind the gap -- a closer look at the security of block ciphers against differential cryptanalysis
- On semantic cutting planes with very small coefficients
- Programming for modular reconfigurable robots
- Conflict-driven answer set solving: from theory to practice
- Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
- Resolution cannot polynomially simulate compressed-BFS
- On SAT instance classes and a method for reliable performance experiments with SAT solvers
- Testing satisfiability of CNF formulas by computing a stable set of points
- Efficient data structures for backtrack search SAT solvers
- Restarts and exponential acceleration of the Davis-Putnam-Loveland-Logemann algorithm: A large deviation analysis of the generalized unit clause heuristic for random 3-SAT
- Toward leaner binary-clause reasoning in a satisfiability solver
- A complete adaptive algorithm for propositional satisfiability
- On the relations between SAT and CSP enumerative algorithms
- Solving satisfiability problems using elliptic approximations -- effective branching rules
- Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
- Partitioning methods for satisfiability testing on large formulas
- About the incremental validation of first-order stratified knowledge-based decision-support systems
- Complete on average Boolean satisfiability
- On the automatizability of resolution and related propositional proof systems
- A sharp threshold in proof complexity yields lower bounds for satisfiability search
- Structured proof procedures
- The complexity of inverting explicit Goldreich's function by DPLL algorithms
- A coupled method of Laplace transform and Legendre wavelets for Lane-Emden-type differential equations
- Formal verification based on Boolean expression diagrams
- New methods for 3-SAT decision and worst-case analysis
- The Multi-SAT algorithm
- Complexity analysis of propositional resolution with autarky pruning
- Solving SAT by algorithm transform of Wu's method
- On the complexity of choosing the branching literal in DPLL
- Resource-constrained project scheduling with activity splitting and setup times
- Accelerating backtrack search with a best-first-search strategy
- Reversible pebble games and the relation between tree-like and general resolution space
- Inference approach based on Petri nets
- Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search
- Bounded-depth Frege complexity of Tseitin formulas for all graphs
- Graph-based construction of minimal models
- Moderate exponential-time algorithms for scheduling problems
- SCL(EQ): SCL for first-order logic with equality
- Accelerating logic-based benders decomposition for railway rescheduling by exploiting similarities in delays
- Deep cooperation of CDCL and local search for SAT
- Characterizing Tseitin-formulas with short regular resolution refutations
- Assessing progress in SAT solvers through the Lens of incremental SAT
- Projection heuristics for binary branchings between sum and product
- Logical cryptanalysis with WDSat
- Automated generation of exam sheets for automated deduction
- A logic-based Benders decomposition for microscopic railway timetable planning
- What convex geometries tell about shattering-extremal systems
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Faradžev Read-type enumeration of non-isomorphic CC systems
- Improved algorithms for the general exact satisfiability problem
- Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions
- Limitations of restricted branching in clause learning
- Propagation via lazy clause generation
- Characterising tree-like Frege proofs for QBF
- A conflict-driven solving procedure for poly-power constraints
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)
