不真
发表于 2025-3-30 10:23:13
Verification in ACL2 of a Generic Framework to Synthesize SAT-Proversork where we define a generic transformation based SAT-prover, and we show how this generic framework can be formalized in the ACL2 logic, making a formal proof of its termination, soundness and completeness. This generic framework can be instantiated to obtain a number of verified and executable SA
COLON
发表于 2025-3-30 16:14:29
http://reply.papertrans.cn/59/5879/587865/587865_52.png
单独
发表于 2025-3-30 20:36:36
Forward Slicing of Multi-paradigm Declarative Programs Based on Partial Evaluationgram understanding, maintenance, debugging, testing, code reuse, etc. This paper introduces the first forward slicing technique for multi-paradigm declarative programs. In particular, we show how program slicing can be defined in terms of online partial evaluation. Our approach clarifies the relatio
FISC
发表于 2025-3-30 23:46:34
http://reply.papertrans.cn/59/5879/587865/587865_54.png
Carcinogenesis
发表于 2025-3-31 04:38:31
Logic Based Program Synthesis and Transformation978-3-540-45013-9Series ISSN 0302-9743 Series E-ISSN 1611-3349
Scleroderma
发表于 2025-3-31 09:02:04
Lecture Notes in Computer Sciencehttp://image.papertrans.cn/l/image/587865.jpg
绝食
发表于 2025-3-31 09:44:54
http://reply.papertrans.cn/59/5879/587865/587865_57.png
变形
发表于 2025-3-31 15:08:28
A Fixed Point Semantics for Logic Programs Extended with CutsIn this paper, we develop a bottom-up fixed point semantics for pure Prolog programs extended with !/0 that allows to reconstruct the operational semantics of a particular goal. Our semantics captures both the order in which solutions are computed by SLD-resolution and their multiplicity.
NAIVE
发表于 2025-3-31 20:26:56
http://reply.papertrans.cn/59/5879/587865/587865_59.png