alcoholism
发表于 2025-3-23 12:39:20
http://reply.papertrans.cn/83/8300/829962/829962_11.png
起草
发表于 2025-3-23 14:43:36
http://reply.papertrans.cn/83/8300/829962/829962_12.png
热心
发表于 2025-3-23 18:53:32
A Certified AC Matching Algorithm,tive. This algorithm is presented by inference rules and these rules have been formally proven sound and complete, and decreasing in the COQ proof assistant while the corresponding algorithm is implemented in the C.ME system. Moreover some preparatory work has been done in COQ, such as proving that
是剥皮
发表于 2025-3-24 01:00:09
Matchbox : A Tool for Match-Bounded String Rewriting,t to an (inverse) match-bounded string rewriting system. . can search for proof or disproof of a Boolean combination of match-height properties of a given rewrite system, and some of its transformed variants. This is applied in various ways to search for proofs of termination and non-termination. .
minion
发表于 2025-3-24 05:51:41
Querying Unranked Trees with Stepwise Tree Automata,omata can express the same monadic queries as monadic Datalog and monadic second-order logic. We prove this result by reduction to the ranked case, via a new systematic correspondence that relates unranked and ranked queries.
拖网
发表于 2025-3-24 09:02:00
http://reply.papertrans.cn/83/8300/829962/829962_16.png
Halfhearted
发表于 2025-3-24 13:55:29
Rewriting for Fitch Style Natural Deductions,ore closely to proofs in ordinary mathematical practice, is given in . We define precisely a Curry-Howard interpretation that maps Fitch style deductions to simply typed terms, and we analyze why it is not an isomorphism. We then describe three reduction relations on Fitch style natural
丰富
发表于 2025-3-24 17:27:09
Efficient ,-Evaluation with Interaction Nets,revious works, we obtain one of the most efficient implementations of this kind to date: out performing existing interaction net implementations, as well as other approaches. We conclude the paper with extensive testing to demonstrate the capabilities of this evaluator.
GRATE
发表于 2025-3-24 21:13:19
Proving Properties of Term Rewrite Systems via Logic Programs,n TRS result in so-called cs-programs, which were originally studied in the context of constraint systems and tree tuple languages. By applying decidability and computability results of cs-programs we obtain new classes of TRS that have nice properties like decidability of unification, regular sets
健谈的人
发表于 2025-3-25 00:21:27
,: A Tool for Proving Termination of Context-Sensitive Rewriting,ting (.) is an example of such a restriction. In ., the replacements in some arguments of the function symbols are permanently forbidden. This paper describes ., a tool which can be used to automatically prove termination of .. The tool implements the generation of the appropriate orderings for prov