Some results and experiments in programming techniques for propositional logic

DOI10.1016/0305-0548(86)90056-0zbMath0641.68140OpenAlexW2092931458MaRDI QIDQ1100931

C. E. Blair, James K. Lowe, Robert G. Jeroslow

Publication date: 1986

Published in: Computers \& Operations Research (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0305-0548(86)90056-0

zbMATH Keywords

propositional logicmathematical programmingtheorem-provingbranch- and-bound

Mathematics Subject Classification ID

Integer programming (90C10) Mechanization of proofs and logical operations (03B35)

Related Items

Inference of a minimum size Boolean function from examples by using a new efficient branch-and-bound approach, A linear-time transformation of linear inequalities into conjunctive normal form, Resolution vs. cutting plane solution of inference problems: Some computational experience, On renamable Horn and generalized Horn functions, Branch-and-cut solution of inference problems in propositional logic, Solving propositional satisfiability problems, An explicit semidefinite characterization of satisfiability for Tseitin instances on toroidal grid graphs, An approach to guided learning of Boolean functions, On the minimum number of logical clauses inferred from examples, A BDD SAT solver for satisfiability testing: An industrial case study, Logic applied to integer programming and integer programming applied to logic, Compact normal forms in propositional logic and integer programming formulations, Projecting systems of linear inequalities with binary variables, Modeling and integer programming techniques applied to propositional calculus, Probabilistic bounds and algorithms for the maximum satisfiability problem, The \(Multi\)-SAT algorithm, Mixed logical-linear programming, Semidefinite resolution and exactness of semidefinite relaxations for satisfiability, MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability, Autark assignments of Horn CNFs, On semidefinite least squares and minimal unsatisfiability, Sensitivity analysis for Horn formulae, An efficient algorithm for the 3-satisfiability problem, Deriving conclusions in expert systems when knowledge is incomplete, A dual algorithm for the satisfiability problem, Algorithms for the maximum satisfiability problem, Computational experience with an interior point algorithm on the satisfiability problem, New methods for computing inferences in first order logic, An exact algorithm for the constraint satisfaction problem: Application to logical inference, Generating logical expressions from positive and negative examples via a branch-and-bound approach

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
• Production rules as a representation for a knowledge-based consultation program
• Modelling with integer variables
• Pivot and Complement–A Heuristic for 0-1 Programming
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory