Theorem proving in propositional logic on vector computers using a generalized Davis-Putnam procedure.
Wen-Tsuen ChenMing-Yi FangPublished in: SC (1990)
Keyphrases
- davis putnam
- propositional logic
- theorem proving
- first order logic
- proof procedure
- inference rules
- quantified boolean formulae
- propositional satisfiability
- theorem prover
- automated reasoning
- knowledge representation
- decision procedures
- belief revision
- predicate calculus
- probabilistic reasoning
- propositional formulas
- knowledge base
- horn clauses
- belief change
- heuristic search