
Browse All Reviews > Theory Of Computation (F) > Mathematical Logic And Formal Languages (F.4) > Mathematical Logic (F.4.1) > Mechanical Theorem Proving (F.4.1...)









110 of 95
Reviews about "Mechanical Theorem Proving (F.4.1...)":

Date Reviewed 

Fundamental proof methods in computer science: a computerbased approach Arkoudas K., Musser D., MIT Press, Cambridge, MA, 2017.Type: Book (9780262035538) An introduction to proof methods in computer science (CS), this book is set apart from other by its reliance on an interactive theorem prover (called Athena) to achieve the task....

Sep 21 2017 

A theorem about computationalism and "absolute" truth Charlesworth A. Minds and Machines 26(3): 205226, 2016. Type: Article Is logical inconsistency (or fallibility) an inherent advantage of the human mind over computers? Does computing need to be logical? Minsky, in a quote reproduced in the paper, thought that, “There’s no reason to assume ... that either...

Jun 2 2017 

Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL Aransay J., Divasón J. Formal Aspects of Computing 28(6): 10051026, 2016. Type: Article Formalization is rapidly evolving from being highly desirable but thought too difficult to be realistic, to being quite feasible and well on its way to being expected. The raw technology of theorem provers certainly is ready. What is still evolvin...

Mar 9 2017 

Synthesis of list algorithms by mechanical proving Drmnesc I., Jebelean T. Journal of Symbolic Computation 69(C): 6192, 2015. Type: Article Program synthesis via extraction of programs from constructive proofs is now very well established, with a large literature base. There are still quite a few hurdles to overcome, but the metatheory has been in place for quite some time now....

Jan 11 2016 

The little prover Friedman D., Eastlund C., The MIT Press, Cambridge, MA, 2015. 248 pp. Type: Book (9780262527958) The goal of this book is to teach readers how to prove that recursive Lisp programs are correct. The method used is based on principles from mathematical logic; it involves identifying basic axioms, theorems, and rules of text transformation, and ...

Dec 9 2015 

A certified reduction strategy for homological image processing Poza M., Domínguez C., Heras J., Rubio J. ACM Transactions on Computational Logic 15(3): Article No. 23, 2014. Type: Article Truelife biomedical images, such as the synapses of neurons, are too large and onerous to process. How should the data structures of huge digital images be reliably condensed without losing their homological properties? Poza et al. propose a spec...

Nov 6 2014 

A framework for testing firstorder logic axioms in program verification Ahn K., Denney E. Software Quality Journal 21(1): 159200, 2013. Type: Article As modeldriven code generators have increased in capability and in performance, so too has their use in missioncritical software development. One benefit of autogenerated code over handcrafted, individually created source code is that it is sim...

Jun 4 2014 

Flow logic for process calculi Nielson H., Nielson F., Pilegaard H. ACM Computing Surveys 44(1): 139, 2012. Type: Article Nielson et al. present an approach using flow logic to represent programming notations in process calculi. Flow logic is usually used in static analysis for language paradigms, including imperative, functional, and concurrent features. The lambda ...

May 30 2012 

Weyl’s predicative classical mathematics as a logicenriched type theory Adams R., Luo Z. ACM Transactions on Computational Logic 11(2): 129, 2010. Type: Article Given proofassistant builders’ renewed interest in foundational issues, revisiting Hermann Weyl’s classic text [1] is a worthy endeavor. Unfortunately, this paper greatly disappoints....

May 28 2010 

Data compression for proof replay Amjad H. Journal of Automated Reasoning 41(34): 193218, 2008. Type: Article Interactive theorem provers suffer from a disadvantage implied by the name: in the proof of a nontrivial theorem, manual guidance by the user is often required. By contrast, Boolean satisfiability (SAT) solvers are powerful tools for propositional...

Aug 20 2009 





