Titlebook: Automated Deduction in Classical and Non-Classical Logics; Selected Papers Ricardo Caferra,Gernot Salzer Conference proceedings 2000 Spring

Pruritus

可耕种

Proving Associative-Commutative Termination Using RPO-Compatible Orderingscursive path ordering (RPO) schemes is desirable, and this property helps in orienting the commonly encountered distributivity axiom as desired. For applications in theorem proving and constraint solving, a total ordering on ground terms involving AC operators is often required. It is shown how the

installment

范围广

Replacement Rules with Definition Detectionerform badly on theorems such as those from set theory that are proven largely by expanding Definitions. The technique of using replacement rules permits automatic proofs of such theorems to be found quickly in many cases. We present a refinement of the replacement rule method which increases its ef

罗盘

On the Complexity of Finite Sorted Algebrasraph isomorphism problem (.). It is easy to see that this fact still holds when sorts are introduced. However, this isomorphism problem is relevant only for algebras (or interpretations) of a fixed signature, and in some cases, according to the signature, is much simpler than the general problem. We

玛瑙