ALB
发表于 2025-3-30 09:12:01
0302-9743the papers are organized into sections on theorem proving, narrowing, logic programming, term rewriting, and higher-order programming.978-3-540-58431-5978-3-540-48791-3Series ISSN 0302-9743 Series E-ISSN 1611-3349
Aphorism
发表于 2025-3-30 15:39:57
http://reply.papertrans.cn/16/1528/152761/152761_52.png
staging
发表于 2025-3-30 19:46:58
http://reply.papertrans.cn/16/1528/152761/152761_53.png
Duodenitis
发表于 2025-3-30 23:31:59
Sufficient completeness and parameterized proofs by induction,lete and the constructors are not free. The method has been implemented in the prover SPIKE. Based on computer experiments, the method appears to be more practical and efficient than inductive theorem proving in non-parameterized specifications. Moreover, SPIKE offers facilities to check and complete definitions.
intangibility
发表于 2025-3-31 03:20:04
http://reply.papertrans.cn/16/1528/152761/152761_55.png
管理员
发表于 2025-3-31 09:04:12
https://doi.org/10.1007/978-1-4471-2377-4 to a given first-order specification is equivalent to the standard validity of the same formula in a suitably enriched specification. As a consequence any proof system for first-order logic can be used to prove the behavioural validity of first-order formulas.
我不死扛
发表于 2025-3-31 11:50:19
https://doi.org/10.1007/978-3-319-75259-4 the solutions of this geometrical system corresponding to the solutions of the original algebraic problem. As a corollary, unification in planar ternary rings is finitary and constitutes a decidable class of problems for which a type conformal algorithm exists.