

automated proof search 
OverviewConnectionsEvolutionDirectionReferences  
DirectionAbstract Strategic thinking is at the intellectual core of the calculus for the 21st century, which is not the mathematical calculus that emerged in the 17th century, but rather the logical calculus that was conceived in the same period by Leibniz, one of the two inventors of the mathematical calculus. Leibniz put great emphasis on a universal language to organize concepts, on rules to guide thinking and on mechanical algorithms to solve problems. The idea of the logical calculus came to theoretical fruition in the first half of the 20th century; it became absolutely vital during the second half of that century in the context of the computing revolution. Proofs, functions and computations are the fundamental components of the logical calculus, but are scattered in logic, mathematics and computer science. Thorough familiarity with these concepts is no longer a privilege of a first rate education cutting across the boundaries of the three disciplines. On the contrary, it is a practical necessity for computer scientists and for students whose subject involves computational modeling, be they biologists, psychologists or economists. For students who reflect on the social impact of computers or conceive of mental processes as computations, it is equally central. Our work aims to contribute to educational practice and research. It contributes to the former by expanding an innovative introduction to logic with a focus on proofs through two deeply integrated parts on functions and computations. It contributes to the latter by using this expanded, fully webbased course, Computational Logic, as a Learning Laboratory to evaluate the efficacy of pedagogical approaches, in particular, our central one of teaching and tutoring strategic thinking. Our approach has its cognitive foundation partially in the computational model of goaldirected logical reasoning; the broader reflective use of logic in mathematical problem solving can, we conjecture, be modeled in extensions of AProS. Thus, the Learning Laboratory also allows us to test, refine and extend the cognitive foundation for strategic thinking. The full discussion can be found here: Strategic Thinking 