Titlebook: Rewriting Techniques and Applications; 11th International C Leo Bachmair Conference proceedings 2000 Springer-Verlag Berlin Heidelberg 2000

竖琴

容易懂得

acrobat

Deriving Theory Superposition Calculi from Convergent Term Rewriting Systemses, in order to make automated theorem proving in these theories more effective. In particular we consider abelian groups and commutative rings. These are difficult for automated theorem provers, since their axioms of associativity, commutativity, distributivity and the inverse law can generate many

PAN

Right-Linear Finite Path Overlapping Term Rewriting Systems Effectively Preserve Recognizabilityerly includes the class of linear generalized semi-monadic TRS and the class of inverse left-linear growing TRS, which are known to effectively preserve recognizability. Approximations by inverse right-linear finite path overlapping TRS are also discussed.

Aggregate

PURG

keloid

HUMP

样式

夹死提手势

The Explicit Representability of Implicit Generalizationsven a disjunction of implicit generalizations ., do there exist terms ..,..., .. , s.t. the ground terms represented by . coincide with the union of the .-ground instances of the terms ..? In this paper, we prove the coNP-completeness of this decision problem.