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)- Long distance Q-resolution with dependency schemes
- Toward leaner binary-clause reasoning in a satisfiability solver
- Portfolios in stochastic local search: efficiently computing most probable explanations in Bayesian networks
- Symmetric matroid polytopes and their generation
- Constructing Bachmair-Ganzinger models
- Tight upper bound on splitting by linear combinations for pigeonhole principle
- Laissez-faire caching for parallel \#SAT solving
- Partitioning methods for satisfiability testing on large formulas
- About the incremental validation of first-order stratified knowledge-based decision-support systems
- Transition systems for model generators -- a unifying approach
- Extended resolution simulates binary decision diagrams
- Matroid enumeration for incidence geometry
- Banishing ultrafilters from our consciousness
- Partitioning methods for satisfiability testing on large formulas
- Editorial: Symbolic computation and satisfiability checking
- A SAT-based preimage analysis of reduced \textsc{Keccak} hash functions
- On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
- Decomposition representations of logical equations in problems of inversion of discrete functions
- New methods for 3-SAT decision and worst-case analysis
- Formally verifying the solution to the Boolean Pythagorean triples problem
- Conflict-directed \(A^{*}\) and its role in model-based embedded systems
- Mind the gap -- a closer look at the security of block ciphers against differential cryptanalysis
- SAT-based bounded model checking for propositional projection temporal logic
- GD-SAT model and crossover line
- Learning to select branching rules in the DPLL procedure for satisfiability
- Characterizing Tseitin-formulas with short regular resolution refutations
- Reflections on Proof Complexity and Counting Principles
- SCL(EQ): SCL for first-order logic with equality
- \(\mathrm P \overset {?} {=} \mathrm{NP}\)
- Generating hard satisfiability problems
- Disjunctive answer set solvers via templates
- 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
- Symbolic techniques in satisfiability solving
- Nagging: A scalable fault-tolerant paradigm for distributed search
- Compiling problem specifications into SAT
- On the power of clause-learning SAT solvers as resolution engines
- Fast congruence closure and extensions
- Accelerating backtrack search with a best-first-search strategy
- New upper bound for the \#3-SAT problem
- Depth lower bounds in Stabbing Planes for combinatorial principles
- DPLL: the core of modern satisfiability solvers
- GridSAT: Design and implementation of a computational grid application
- On CDCL-Based Proof Systems with the Ordered Decision Strategy
- SCL(EQ): SCL for first-order logic with equality
- On the complexity of choosing the branching literal in DPLL
- Modular inference of linear types for multiplicity-annotated arrows
- Challenges in Constraint-Based Analysis of Hybrid Systems
- Solving satisfiability problems with preferences
- Generalized conflict-clause strengthening for satisfiability solvers
- Empirical study of the anatomy of modern SAT solvers
- Reconstructing (h,v)-convex 2-dimensional patterns of objects from approximate horizontal and vertical projections.
- Towards NP-P via proof complexity and search
- A coupled method of Laplace transform and Legendre wavelets for Lane-Emden-type differential equations
- A numerical method for Lane-Emden equations using hybrid functions and the collocation method
- Machine learning for first-order theorem proving
- Linear-Time Algorithm for Quantum 2SAT
- Regular-SAT: A many-valued approach to solving combinatorial problems
- A taxonomy of exact methods for partial Max-SAT
- The state of SAT
- Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions
- On the structure of some classes of minimal unsatisfiable formulas
- BerkMin: A fast and robust SAT-solver
- Generalizing DPLL and satisfiability for equalities
- New methods for proving the impossibility to solve problems through reduction of problem spaces
- Accelerating logic-based benders decomposition for railway rescheduling by exploiting similarities in delays
- Certified SAT solving with GPU accelerated inprocessing
- MAX SAT approximation beyond the limits of polynomial-time approximation
- Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic
- Conformant planning as a case study of incremental QBF solving
- SatEx: A web-based framework for SAT experimentation
- John McCarthy's legacy
- Towards an efficient library for SAT: A manifesto
- An efficient approach to solving random \(k\)-SAT problems
- A parallelization scheme based on work stealing for a class of SAT solvers
- On preprocessing techniques and their impact on propositional model counting
- Typical case complexity of satisfiability algorithms and the threshold phenomenon
- Chain, generalization of covering code, and deterministic algorithm for \(k\)-SAT
- The Complexity of Propositional Proofs
- Proving unsatisfiability of CNFs locally
- Computation of Renameable Horn Backdoors
- An exponential lower bound for the pure literal rule
- Multi-threaded ASP solving with clasp
- Equivalent literal propagation in the DLL procedure
- On the limit of branching rules for hard random unsatisfiable 3-SAT
- SAT problems with chains of dependent variables
- Finding kernels or solving SAT
- Creating non-minimal triangulations for use in inference in mixed stochastic/deterministic graphical models
- Computing weighted solutions in ASP: representation-based method vs. search-based method
- Engineering constraint solvers for automatic analysis of probabilistic hybrid automata
- Exact algorithms for exact satisfiability and number of perfect matchings
- Resource-constrained project scheduling with activity splitting and setup times
- First order Stålmarck. Universal lemmas through branch merges
- Deep cooperation of CDCL and local search for SAT
- Logical cryptanalysis with WDSat
- Projection heuristics for binary branchings between sum and product
- A review on declarative approaches for constrained clustering
- A competitive and cooperative approach to propositional satisfiability
- Substitutions into propositional tautologies
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)
