Content deleted Content added
mNo edit summary Tags: Mobile edit Mobile app edit iOS app edit |
Citation bot (talk | contribs) Alter: pages. Add: s2cid. Formatted dashes. | Use this bot. Report bugs. | Suggested by AManWithNoPlan | Linked from User:AManWithNoPlan/sandbox4 | #UCB_webform_linked 55/1831 |
||
Line 19:
=== Efficiency and complexity of proof procedures ===
Theorem proving often benefits from decision procedures and theorem proving algorithms, whose correctness has been extensively analyzed. A straightforward way of implementing these procedures in an LCF approach requires such procedures to always derive outcomes from the axioms, lemmas, and inference rules of the system, as opposed to directly computing the outcome. A potentially more efficient approach is to use reflection to prove that a function operating on formulas always gives correct result.<ref>{{cite report |last1=Boyer |first1=Robert S |last2=Moore |first2=J Strother |title=Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures |publisher=Technical Report CSL-108, SRI Projects 8527/4079 |pages=
== Influences ==
Line 44:
| volume = 78
| publisher = Springer |___location=Berlin Heidelberg
| isbn = 978-3-540-09724-2
}}
* {{cite book
| last = Gordon
| |||