## An alternative for handling AC

- A method for efficiently handling associativity and commutativity (AC) in implementations of (equational) theorem provers without incorporating AC as an underlying theory will be presented. The key of substantial efficiency gains resides in a more suitable representation of permutation-equations (such as f(x,f(y,z))=f(y,f(z,x)) for instance). By representing these permutation-equations through permutations in the mathematical sense (i.e. bijective func- tions :{1,..,n} {1,..,n}), and by applying adapted and specialized inference rules, we can cope more appropriately with the fact that permutation-equations are playing a particular role. Moreover, a number of restrictions concerning application and generation of permuta- tion-equations can be found that would not be possible in this extent when treating permu- tation-equations just like any other equation. Thus, further improvements in efficiency can be achieved.

Author: | Matthias Fuchs |
---|---|

URN (permanent link): | urn:nbn:de:hbz:386-kluedo-3855 |

Serie (Series number): | SEKI Report (94,3) |

Document Type: | Article |

Language of publication: | English |

Year of Completion: | 1994 |

Year of Publication: | 1994 |

Publishing Institute: | Technische Universität Kaiserslautern |

Date of the Publication (Server): | 1999/08/24 |

Faculties / Organisational entities: | Fachbereich Informatik |

DDC-Cassification: | 0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik |

Licence (German): | Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011 |