blackout
发表于 2025-3-25 06:56:31
http://reply.papertrans.cn/59/5879/587880/587880_21.png
anaerobic
发表于 2025-3-25 10:26:01
Guiding program development systems by a connection based proof strategy,rategy extends Bibel‘s connection method for classical predicate logic. It generates a matrix proof which will then be transformed into a proof within a standard sequent calculus. Thus we can use an efficient proof method to guide the development of constructive proofs in interactive proof/program d
OWL
发表于 2025-3-25 11:50:30
http://reply.papertrans.cn/59/5879/587880/587880_23.png
cataract
发表于 2025-3-25 19:25:35
Logic program synthesis by induction over Horn Clauses,ork by Feferman , and allows constructive proof by induction over the minimal Herbrand model of a set of Horn Clauses. This is an important addition to the Whelk system, because it admits reasoning about and synthesis from “real” logic programs, whereas previously the system was limited to induct
值得尊敬
发表于 2025-3-25 21:40:49
http://reply.papertrans.cn/59/5879/587880/587880_25.png
CIS
发表于 2025-3-26 01:44:42
An opportunistic approach for logic program analysis and optimisation using enhanced schema-based tattempted, either by examining its procedures in an isolated fashion, or by checking for conjunctions within clauses that can be used as joint specifications. Opportunities are represented as ., generic descriptions of inefficient programming constructs and of how these should be altered in order to
裙带关系
发表于 2025-3-26 06:10:57
http://reply.papertrans.cn/59/5879/587880/587880_27.png
Irremediable
发表于 2025-3-26 10:30:51
Towards a complete proof procedure to prove properties of normal logic programs under the completiorams and an extension to normal ones was proposed afterwards. The correctness of the extended framework has been shown and in this paper we investigate the question of its completeness. We give results at the propositional level and discuss a possible alternative to achieve completeness at the non p
otic-capsule
发表于 2025-3-26 13:17:00
Termination of logic programs using semantic unification, the logic program follows from termination of the derived constructor system. Thereafter, we present a new technique to prove termination of constructor systems. In the technique semantic unification is used. Thus, surprisingly, semantic unification can be used For giving termination proofs for log
定点
发表于 2025-3-26 20:53:04
On the mechanics of metasystem hierarchies in program transformation,eason about the mechanics of hierarchies of program transformers and to describe applications that go beyond the ‘classical’ Futamura projections. This paper identifies and clarifies foundational issues involved in multi-level metasystem hierarchies. After studying the role of abstraction, encoding,