Automated Theorem Proving

← Back to Domain-Specific Abstractions by Domain

1 domain-specific abstractions whose origin domain is Automated Theorem Proving.

• Davis–Putnam Algorithm — Decide clausal satisfiability by eliminating variables with resolution while preserving whether the clause set has a model.