exophthalmos 发表于 2025-3-23 12:06:11

Building proofs by analogy via the Curry-Howard Isomorphism,oward Isomorphism is used to represent proof constructions in a term-functional language and to specify analogies by transformation rules on these terms. The method has the advantage to admit . formalization and to make use of well-known techniques like higher-order unification.

厌恶 发表于 2025-3-23 15:32:03

On deductive planning and the frame problem, frame problem, ie. the technical problem of how to formalize the assumption that unless an action explicitly causes a certain fact to hold or not to hold, the facts are preserved by the action. It is shown that there is no need to explicitly state frame axioms, ie. axioms which deal with the frame

Hiatus 发表于 2025-3-23 18:09:46

http://reply.papertrans.cn/59/5880/587906/587906_13.png

dithiolethione 发表于 2025-3-24 01:53:55

A procedure for automatic proof nets construction,o make logic programming or to program with proofs, a better comprehension of the proof construction process in this framework is necessary. We propose a new algorithm to construct automatically a proof net for a given sequent in MLL and its proofs of termination, correctness and completeness. It ca

incubus 发表于 2025-3-24 03:37:05

http://reply.papertrans.cn/59/5880/587906/587906_15.png

侵害 发表于 2025-3-24 09:22:36

Towards probabilistic knowledge bases,uirements. First, it must coincide with the intuitive understanding of the given information, and second, the semantics must be computationally tractable. We show that our semantics fulfills the first requirement and we formally verify that our fixpoint semantics reduces to the usual fixpoint semant

Peak-Bone-Mass 发表于 2025-3-24 13:27:36

http://reply.papertrans.cn/59/5880/587906/587906_17.png

的’ 发表于 2025-3-24 17:38:33

http://reply.papertrans.cn/59/5880/587906/587906_18.png

CT-angiography 发表于 2025-3-24 20:04:33

Controlling redundancy in large search spaces: Argonne-style theorem proving through the years,llaborators have developed a long series of theorem-proving systems with which to explore this fascinating field. Since the first systems of the mid-sixties, many features have changed of course, but others, perhaps the most fundamental, have remained the same. We survey here some of the history of

unstable-angina 发表于 2025-3-24 23:25:21

http://reply.papertrans.cn/59/5880/587906/587906_20.png
页: 1 [2] 3 4 5 6 7
查看完整版本: Titlebook: Logic Programming and Automated Reasoning; International Confer Andrei Voronkov Conference proceedings 1992 Springer-Verlag Berlin Heidelbe