祖先
发表于 2025-3-25 06:45:48
http://reply.papertrans.cn/83/8300/829949/829949_21.png
浮雕宝石
发表于 2025-3-25 08:54:12
A de Bruijn Notation for Higher-Order Rewritingbut also for metaterms, which are the syntactical objects used to express general higher-order rewrite systems. We give formal translations from higher-order rewriting with names to higher-order rewriting with de Bruijn indices, and vice-versa. These translations can be viewed as an . in programming
不能仁慈
发表于 2025-3-25 14:38:56
Rewriting Techniques in Theoretical Physicsn the field of statistical physics. Our method automatically helps in validating some conjectures due to physicists, such as conjectures stating that a set of equations completely describes a finite given quotient of ... In a first step, we show that in the cases we are interested in, the usual pres
连锁
发表于 2025-3-25 16:27:08
Normal Forms and Reduction for Theories of Binary Relationslid in the standard model of sets and also define a hierarchy of equational axiomatisations stratifying the standard theory. By working directly with a presentation of relation-expressions as . we are able to define a notion of reduction which is confluent and strongly normalising, in sharp contrast
Chameleon
发表于 2025-3-25 20:45:48
Parallelism Constraintssent a semi-decision procedure enumerating all “most general unifiers” of a parallelism constraint and prove it sound and complete. In contrast to all known procedures for context unification, the presented procedure terminates for the important fragment of dominance constraints and performs reasona
增长
发表于 2025-3-26 01:16:08
Linear Higher-Order Matching Is NP-Complete is exactly one free occurrence of . in .). We prove that this problem is decidable by showing that it belongs to NP. Then we prove that this problem is in fact NP-complete. Finally, we discuss some heuristics for a practical algorithm.
Ornithologist
发表于 2025-3-26 07:13:12
Standardization and Confluence for a Lambda Calculus with Generalized Applicationsem with non-trivial critical pairs, confluence is established by studying triangle properties that allow to treat permutative reductions modularly and could be extended to more complex term systems with permutations. Standardization is shown by means of an inductive definition of standard reduction
phlegm
发表于 2025-3-26 11:35:17
http://reply.papertrans.cn/83/8300/829949/829949_28.png
易于
发表于 2025-3-26 15:43:04
http://reply.papertrans.cn/83/8300/829949/829949_29.png
STALL
发表于 2025-3-26 18:33:19
The Explicit Representability of Implicit Generalizations that . represents all .-ground instances of . that are not instances of any term .. on the right-hand side. More generally, we can also consider disjunctions . of implicit generalizations, where . contains all ground terms from . that are contained in at least one of the implicit generalizations ..