First-Order Sentence Satisfiability Task
Jump to navigation
Jump to search
A First-Order Sentence Satisfiability Task is a Satisfiability Task that is restricted to First-Order Sentences.
- Context:
- It can involve the:
- Resolution Rule Method, where the Resolution Rule is applied and if an Empty Clause is generated then Clause Set is Unsatisfiable.
- Partial-Instantiation Method,
- It can involve the:
- See: First-Order Logic Inference Task, Herbrand Universe.