Automated deduction with associative-commutative operators | Zendy

M. Rusinowitch | Zendy; Laurent Vigneron | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Automated deduction with associative-commutative operators

Author(s) -

M. Rusinowitch,

Laurent Vigneron

Publication year - 1995

Publication title -

applicable algebra in engineering communication and computing

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.558

H-Index - 35

eISSN - 1432-0622

pISSN - 0938-1279

DOI - 10.1007/bf01270929

Subject(s) - rule of inference , associative property , axiom , commutative property , unification , inference , computer science , theoretical computer science , completeness (order theory) , natural deduction , tree (set theory) , mathematics , congruence (geometry) , algebra over a field , algorithm , discrete mathematics , programming language , artificial intelligence , pure mathematics , combinatorics , mathematical analysis , geometry

We propose a new inference system for automated deduction with equality and associative commutative operators. This system is an extension of the ordered paramodulation strategy. However, rather than using associativity and commutativity as the other axioms, they are handled by the AC-unification algorithm and the inference rules. Moreover, we prove the refutational completeness of this system without needing the functional reflexive axioms or AC-axioms. Such a result is obtained by semantic tree techniques. We also show that the inference system is compatible with simplification rules.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research