In abstract algebra, a structure is said to be Noetherian if it does not admit infinite strictly ascending chains of congruences. In this paper, we adapt this notion to first-ord...
Constraint solvers are key modules in many systems with reasoning capabilities (e.g., automated theorem provers). To incorporate constraint solvers in such systems, the capability ...
Abstract. We propose a new class of tree automata, called tree automata with normalization (TAN). This framework extends equational tree automata, and improved the results of them:...
We present a simple logic that combines, in a conservative way, the implicative fragments of both classical and intuitionistic logics, thus settling a problem posed by Dov Gabbay i...
Abstract. Innermost context-sensitive rewriting has been proved useful for modeling computations of programs of algebraic languages like Maude, OBJ, etc. Furthermore, innermost ter...