progestin
发表于 2025-3-25 03:33:13
http://reply.papertrans.cn/59/5880/587904/587904_21.png
output
发表于 2025-3-25 11:13:53
RISC-CLP(CF) constraint logic programming over complex functions, who often reason/compute with constraints over complex functions, such as functional equalities, differential equations, etc. Constraints are solved by iterating several solving methods such as Laplace transformation, non-linear equation solving, etc. A prototype has been built and is illustrated i
acheon
发表于 2025-3-25 13:12:43
http://reply.papertrans.cn/59/5880/587904/587904_23.png
令人发腻
发表于 2025-3-25 16:24:20
Higher-order rigid E-unification,quational theory, is undecidable. We propose to rigidifyit, to get a resource-bounded decidable unification problem (with arbitrary high bounds), providing a complete higher-order E-unification procedure. The techniques are inspired from Gallier‘s rigid E-unification and from Dougherty and Johann‘s
fringe
发表于 2025-3-25 20:02:03
http://reply.papertrans.cn/59/5880/587904/587904_25.png
commonsense
发表于 2025-3-26 01:13:20
Higher-Order Abstract Syntax with induction in Coq,rder) injection principle, which asserts that equal terms have equal heads and equal sons, and the extensionality principle, which asserts that functional terms which are pointwise equal are equal. Higher-order abstract syntax is implemented for instance in the Edinburgh Logical Framework and the ab
Schlemms-Canal
发表于 2025-3-26 06:00:50
http://reply.papertrans.cn/59/5880/587904/587904_27.png
Synapse
发表于 2025-3-26 10:53:46
Constraint logic programming in the sequent calculus,on of constraints into a fragment of intuitionistic logic. Constrained SLD resolution corresponds to a complete proof search in the amalgamated logic. The framework provides not only the logical account on the definitional semantics towards CLP but also a general way to integrate constraints into va
带来
发表于 2025-3-26 13:58:18
On conditional rewrite systems with extra variables and deterministic logic programs,’. If such a system . is quasi-reductive then → . is decidable and terminating. We develop a critical pair criterion to prove confluence if . is quasi-reductive and strongly deterministic. We apply our results to prove Horn clause programs to be uniquely terminating.
反感
发表于 2025-3-26 19:30:45
A bottom-up reconstruction of the well-founded semantics for disjunctive logic programs, it is closer to a procedural semantics than to the elegant fixpoint definition of the well-founded semantics for normal logic programs. In the present paper, we propose a declarative, bottom-up fixpoint definition of the well-founded semantics for disjunctive logic programs. Our construction of the