Sciweavers

INFORMATICALT
2010
103views more  INFORMATICALT 2010»
13 years 3 months ago
Formal Correctness Proof for DPLL Procedure
The DPLL procedure for the SAT problem is one of the fundamental algorithms in computer science, with many applications in a range of domains, including software and hardware veriď...
Filip Maric, Predrag Janicic
AIEDU
2005
93views more  AIEDU 2005»
13 years 5 months ago
The Logic-ITA in the Classroom: A Medium Scale Experiment
This paper presents the experiment and consequent evaluation of introducing the Logic-ITA in a second year tertiary undergraduate class. The Logic-ITA is a web-based Intelligent Te...
Kalina Yacef
LPAR
1999
Springer
13 years 9 months ago
Proofs About Lists Using Ellipsis
In this paper we explore the use of ellipsis in proofs about lists. We present a higher-order formulation of elliptic formulae, and describe its implementation in the λClam proof ...
Alan Bundy, Julian Richardson
MKM
2009
Springer
13 years 9 months ago
Formal Proof: Reconciling Correctness and Understanding
Hilbert’s concept of formal proof is an ideal of rigour for mathematics which has important applications in mathematical logic, but seems irrelevant for the practice of mathemati...
Cristian S. Calude, Christine Müller