LPAR
2005
Springer
14 years 6 months ago
2005
Springer
Abstract. The main goal of this paper is to apply rewriting termination technology —enjoying a quite mature set of termination results and tools— to the problem of proving auto...
LPAR
2005
Springer
14 years 6 months ago
2005
Springer
We describe a sound, terminating, and complete matching algorithm for terms built over flexible arity function symbols and context, function, sequence, and individual variables. C...
LPAR
2005
Springer
14 years 6 months ago
2005
Springer
Abstract. Earlier we introduced Constraint Lambda Calculi which integrate constraint solving with functional programming for the simple case where the constraint solver produces no...
LPAR
2005
Springer
14 years 6 months ago
2005
Springer
LPAR
2005
Springer
14 years 6 months ago
2005
Springer
We present an algorithm for the conversion of very weak alternating Büchi automata into nondeterministic Büchi automata (NBA), and we introduce a local optimization criterion fo...
LPAR
2005
Springer
14 years 6 months ago
2005
Springer
In this paper the Recursive Path Ordering is adapted for proving termination of rewriting incrementally. The new ordering, called Recursive Path Ordering with Modules, has as ingre...
LPAR
2005
Springer
14 years 6 months ago
2005
Springer
Abstract. We discuss a collection of mechanized formal proofs of symmetric key block encryption algorithms (AES, MARS, Twofish, RC6, Serpent, IDEA, and TEA), performed in an imple...
LPAR
2005
Springer
14 years 6 months ago
2005
Springer
We investigate some syntactic properties of Wadler’s dual calculus, a term calculus which corresponds to classical sequent logic in the same way that Parigot’s λµ calculus co...
LPAR
2005
Springer
14 years 6 months ago
2005
Springer
Abstract. We distill Penrose’s argument against the “artificial intelligence premiss”, and analyze its logical alternatives. We then clarify the different positions one can...
LPAR
2005
Springer
14 years 6 months ago
2005
Springer
Abstract. We present new careful semantics within Dung’s theory of argumentation. Under such careful semantics, two arguments cannot belong to the same extension whenever one of ...