Automated Reasoning

← Back to Domain-Specific Abstractions by Domain

1 domain-specific abstractions whose origin domain is Automated Reasoning.

• Model elimination — A goal-directed automated theorem-proving calculus that extends resolution with ancestor links and a chain-based proof state.