The shift to semantic symmetries is motivated by the fact that, in contrast with syntactic symmetries, these are preserved under standard inference rules such as resolution. It is then possible to attach groups of semantic symmetries to sets of ground clauses. These groups can provide information useful to inference, as illustrated by three “symmetric” rules. These rules are to be applied in well-defined, disjoint cases, they simplify both the set of clauses and the attached group, they use standard and efficient techniques from computational group theory, and therefore they can be easily mechanised. A prototype GAP implementation is described, and an example developed. Finally, some complexity results concerning the computation of semantic symmetries are given.
CITATION STYLE
De la Tour, T. B. (1996). Ground resolution with group computations on semantic symmetries. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1104, pp. 478–492). Springer Verlag. https://doi.org/10.1007/3-540-61511-3_108
Mendeley helps you to discover research relevant for your work.