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 (30)

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

This page was built for publication: Some results and experiments in programming techniques for propositional logic