谦卑
发表于 2025-3-28 14:50:05
http://reply.papertrans.cn/17/1664/166317/166317_41.png
上腭
发表于 2025-3-28 20:31:43
Blocking and Other Enhancements for Bottom-Up Model Generation Methodsrmations of first-order problems into a certain implicational form, namely range-restricted clauses. These refine existing transformations to range-restricted form by extending the domain of interpretation with new Skolem terms in a more careful and deliberate way. Our transformations also extend BU
一条卷发
发表于 2025-3-28 22:54:32
The MathServe System for Semantic Web Reasoning Servicesspread use of automated reasoning techniques requires tools that are easy to use and support standardised protocols and data exchange formats. In the first author presented the MathWeb Software Bus, a first step towards re-usable reasoning services. The MathWeb-SB had several drawbacks which lim
牵连
发表于 2025-3-29 04:00:20
System Description: GCLCprover + GeoThmsen — Euclidean) with its standard models (e.g., Cartesian model) and corresponding illustrations. These tools are used in teaching and studying geometry, some of them also for producing digital illustrations. The common experience is that dynamic geometry tools significantly help students to acquire
Amylase
发表于 2025-3-29 09:16:10
http://reply.papertrans.cn/17/1664/166317/166317_45.png
NEX
发表于 2025-3-29 13:16:36
Extending the TPTP Language to Higher-Order Logic with Automated Parser Generationmbda-calculus expressions, is presented. The purpose of the system is to facilitate sharing of theorem-proving problems in higher-order logic among many researchers. Design goals are discussed. BNF2, a new specification language, is presented. Unix/Linux scripts translate the specification document
disciplined
发表于 2025-3-29 16:41:58
Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semanticsand extensible. We factor HOL into a constructive core plus axioms of excluded middle and choice. We similarly factor standard set theory, ZFC, into a constructive core, IZF, and axioms of excluded middle and choice. Then we provide the standard set-theoretic semantics in such a way that the constru
不可磨灭
发表于 2025-3-29 19:52:11
Towards Self-verification of HOL Lighto be quite feasible. We would like to formally verify (i) that the abstract HOL logic is indeed correct, and (ii) that the OCaml code does correctly implement this logic. We have performed a full verification of an imperfect but quite detailed model of the basic HOL Light core, without definitional
ungainly
发表于 2025-3-30 01:12:31
An Interpretation of Isabelle/HOL in HOL Lightle directly in the HOL Light object logic. The interpretation thus takes the form of a set of elaboration rules, where features of the Isabelle logic that cannot be represented directly are elaborated to functors in OCaml. We demonstrate the effectiveness of the interpretation via an implementation,
Amendment
发表于 2025-3-30 08:02:19
http://reply.papertrans.cn/17/1664/166317/166317_50.png