A parallel approach for theorem proving in propositional logic

DOI10.1016/0020-0255(87)90005-3MaRDI QIDQ1102766zbMATH OpenOpenAlexFDO

Authors Wen-Tsuen Chen, Lung-Lung Liu

Publication date 1987

Published in Information Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0255(87)90005-3

zbMATH Keywords

divide-and-conquer strategyNP-completeparallel proof procedurepipeliningpropositional logictheorem proving

Mathematics Subject Classification ID

Classical propositional logic (03B05) Mechanization of proofs and logical operations (03B35) Theory of operating systems (68N25) Analysis of algorithms and problem complexity (68Q25)

Review text

The divide-and-conquer strategy and a pipelining discipline are applied to theorem proving in propositional logic. The strategy is itself logically complete and sound. Based on this strategy a parallel proof procedure can be constructed. With a pipelined execution model, we show that the processing time using our parallel approach to solve such an NP- complete problem is of O(mn), where m is the number of clauses and n is the number of distinct Boolean variables in the given formula. The approach is simpler than those using explicit inference rules, since the deductions are performed implicitly by only simple checking and deleting operations on each clause.

Recommendations

• An efficient procedure for theorem proving in propositional logic on vector computers
• A constant time algorithm for theorem proving in propositional logic on reconfigurable meshes
• Parallel cooperative propositional theorem proving
• scientific article; zbMATH DE number 4180829
• PARTHENON: A parallel theorem prover for non-horn clauses

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• scientific article; zbMATH DE number 3881899 (Why is no real title available?)
• scientific article; zbMATH DE number 3848585 (Why is no real title available?)
• scientific article; zbMATH DE number 3690676 (Why is no real title available?)
• scientific article; zbMATH DE number 3481857 (Why is no real title available?)
• scientific article; zbMATH DE number 3566230 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• The Specialization of Programs by Theorem Proving

Cited in

(13)

• PARTHENON: A parallel theorem prover for non-horn clauses
• A constant time algorithm for theorem proving in propositional logic on reconfigurable meshes
• Parallelization of a hyper-linking-based theorem prover
• P-Prolog: A parallel logic language based on exclusive relation
• The Multi-SAT algorithm
• Parallel cooperative propositional theorem proving
• Parallel inference search in logical calculus based on the algebraic programming system
• scientific article; zbMATH DE number 4180829 (Why is no real title available?)
• scientific article; zbMATH DE number 3945375 (Why is no real title available?)
• scientific article; zbMATH DE number 4047184 (Why is no real title available?)
• An evolutionary algorithm for theorem proving in propositional logic
• A cooperative parallelization approach for property-directed \(k\)-induction
• An efficient procedure for theorem proving in propositional logic on vector computers

This page was built for publication: A parallel approach for theorem proving in propositional logic

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