Set-Blocked Clause and Extended Set-Blocked Clause in First-Order Logic
Due to scale and complexity of first-order formulas, simplifications play a very important role in first-order theorem proving, in which removal of clauses and literals identified as redundant is a significant component. In this paper, four types of clauses with the local redundancy property were pr...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2018-10-01
|
| Series: | Symmetry |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2073-8994/10/11/553 |