Meta-extract: Using Existing Facts in Meta-reasoning

Kaufmann, M; Swords, S

Kaufmann, M (reprint author), Univ Texas Austin, Dept Comp Sci, Austin, TX 78712 USA.

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017; (249): 47

Abstract

ACL2 has long supported user-defined simplifiers, so-called metafunctions and clause processors, which are installed when corresponding rules of class......

Full Text Link