@inproceedings(ACP-01-a, author = "Andreas Abel and Bor-Yuh Evan Chang and Frank Pfenning", year = "2001", title = "Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic", editor = "Uwe Egly and A. Fiedler and Helmut Horacek and Stephan Schmitt", booktitle = "Proceedings of the Workshop on Proof Transformations, Proof Presentations and Complexity of Proofs (PTP'01)", publisher = "Universit\'{a} degli studi di Siena", ) @incollection(Aleven2000, author = "Vincent Aleven and Kenneth Koedinger", year = "2000", title = "Limitations of Student Control: Do Students Know when They Need Help?", editor = "Gilles Gauthier and Claude Frasson and Kurt VanLehn", booktitle = "Intelligent Tutoring Systems", series = "Lecture Notes in Computer Science", volume = "1839", publisher = "Springer Berlin / Heidelberg", pages = "292--303", url = "http://dx.doi.org/10.1007/3-540-45108-0_33", ) @book(actrtheory, author = "John Robert Anderson", year = "1993", title = "Rules of the mind", publisher = "Lawrence Erlbaum Associates", address = "Hillsdale, NJ", ) @inproceedings(andrews80, author = "Peter B. Andrews", year = "1980", title = "Transforming matings into natural deduction proofs", booktitle = "Proceedings of the 5th Conference on Automated Deduction (CADE)", series = "LNCS 87", publisher = "Springer", pages = "375--393", url = "http://dx.doi.org/10.1007/3-540-10009-1_22", ) @inproceedings(Ashley02teachingcase-based, author = "Kevin D. Ashley and Ravi Desai and John M. Levine", year = "2002", title = "Teaching Case-Based Argumentation Concepts using Dialectic Arguments vs. Didactic Explanations", booktitle = "In Proceedings of the Intelligent Tutoring Systems Conference", publisher = "Springer", pages = "585--595", url = "http://dx.doi.org/10.1007/3-540-47987-2_60", ) @article(AspinallDenneyLueth10, author = "David Aspinall and Ewen Denney and Christoph L\"{u}th", year = "2010", title = "Tactics for Hierarchical Proofs", journal = "Journal Mathematics in Computer Science", volume = "3", pages = "309--330", url = "http://dx.doi.org/10.1007/s11786-010-0025-6", ) @inproceedings(ABDMW-05-a, author = "Serge Autexier and Christoph Benzm\"uller and Dominik Dietrich and Andreas Meier and Claus-Peter Wirth", year = "2006", title = "A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity", editor = "Kohlhase", pages = "126--142", url = "http://dx.doi.org/10.1007/11618027_9", ) @inproceedings(DBLP:conf/itp/AutexierD10, author = "Serge Autexier and Dominik Dietrich", year = "2010", title = "A Tactic Language for Declarative Proofs", editor = "Matt Kaufmann and Lawrence C. Paulson", booktitle = "Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings", series = "Lecture Notes in Computer Science", volume = "6172", publisher = "Springer", pages = "99--114", url = "http://dx.doi.org/10.1007/978-3-642-14052-5_9", ) @inproceedings(AF-05-a, author = "Serge Autexier and Armin Fiedler", year = "2006", title = "Textbook Proofs Meet Formal Logic - The Problem of Underspecification and Granularity", editor = "Kohlhase", pages = "96--110", url = "http://dx.doi.org/10.1007/11618027_7", ) @article(Back2009, author = "Ralph-Johan Back", year = "2010", title = "Structured derivations: a unified proof style for teaching mathematics", journal = "Formal Asp. Comput.", volume = "22", number = "5", pages = "629--661", url = "http://dx.doi.org/10.1007/s00165-009-0136-5", ) @article(Back96structuredcalculational, author = "Ralph-Johan Back and Jim Grundy and Joakim von Wright", year = "1997", title = "Structured Calculational Proof", journal = "Formal Asp. Comput.", volume = "9", number = "5-6", pages = "469--483", url = "http://dx.doi.org/10.1007/BF01211456", ) @inproceedings(DBLP:conf/its/BarnesS08, author = "Tiffany Barnes and John C. Stamper", year = "2008", title = "Toward Automatic Hint Generation for Logic Proof Tutoring Using Historical Student Data", editor = "Beverly Park Woolf and Esma A\"{\i }meur and Roger Nkambou and Susanne P. Lajoie", booktitle = "Intelligent Tutoring Systems, 9th International Conference, ITS 2008, Montreal, Canada, June 23-27, 2008, Proceedings", series = "Lecture Notes in Computer Science", volume = "5091", publisher = "Springer", pages = "373--382", url = "http://dx.doi.org/10.1007/978-3-540-69132-7_41", ) @article(BarnesAndStamper2010, author = "Tiffany Barnes and John C. Stamper", year = "2010", title = "Automatic Hint Generation for Logic Proof Tutoring Using Historical Data", journal = "Educational Technology \& Society", volume = "13", number = "1", pages = "3--12", ) @inproceedings(conf/lpar/Beeson92, author = "Michael Beeson", year = "1992", title = "Mathpert: Computer Support for Learning Algebra, Trig, and Calculus.", editor = "Andrei Voronkov", booktitle = "LPAR", series = "Lecture Notes in Computer Science", volume = "624", publisher = "Springer", pages = "454--456", url = "http://dx.doi.org/10.1007/BFb0013085", ) @inproceedings(C25, author = "Christoph Benzm{\"u}ller and Dominik Dietrich and Marvin Schiller and Serge Autexier", year = "2007", title = "Deep Inference for Automated Proof Tutoring", editor = "Joachim Hertzberg and Michael Beetz and Roman Englert", booktitle = "KI 2007: Advances in Artificial Intelligence. 30th Annual German Conference on AI", series = "LNAI", volume = "4667", publisher = "Springer", pages = "435--439", url = "http://dx.doi.org/10.1007/978-3-540-74565-5_34", ) @inproceedings(dialogcorpusLREC06, author = "Christoph Benzm{\"u}ller and Helmut Horacek and Henri Lesourd and Ivana Kruijff-Korbayov{\'a} and Marvin Schiller and Magdalena Wolska", year = "2006", title = "A corpus of tutorial dialogs on theorem proving; the influence of the presentation of the study-material", booktitle = "Proceedings of International Conference on Language Resources and Evaluation (LREC 2006)", publisher = "ELDA", address = "Genova, Italy", ) @inproceedings(C22, author = "Christoph Benzm{\"u}ller and Helmut Horacek and Henri Lesourd and Ivana Kruijff-Korbayov{\'a} and Marvin Schiller and Magdalena Wolska", year = "2006", title = "DiaWOz-{I}{I} - A tool for wizard-of-oz experiments in mathematics", editor = "Christian Freksa and Michael Kohlhase and Kerstin Schill", booktitle = "KI 2006: Advances in Artificial Intelligence. 29th Annual German Conference on AI", series = "LNAI", volume = "4314", publisher = "Springer", url = "http://dx.doi.org/10.1007/978-3-540-69912-5_13", ) @proceedings(DBLP:conf/tphol/1999, editor = "Yves Bertot and Gilles Dowek and Andr{\'e} Hirschowitz and C. Paulin and Laurent Th{\'e}ry", year = "1999", title = "Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings", series = "Lecture Notes in Computer Science", volume = "1690", publisher = "Springer", url = "http://dx.doi.org/10.1007/3-540-48256-3", ) @article(DBLP:journals/jar/BillingsleyR07, author = "William Billingsley and Peter Robinson", year = "2007", title = "Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book", journal = "J. Autom. Reasoning", volume = "39", number = "2", pages = "181--218", url = "http://dx.doi.org/10.1007/s10817-007-9072-3", ) @inproceedings(buggyrules, author = "John Seely Brown and Kurt VanLehn", year = "1980", title = "Repair theory: A generative theory of bugs in procedural skills", booktitle = "Cognitive Science", volume = "4", pages = "379--426", url = "http://dx.doi.org/10.1207/s15516709cog0404_3", ) @proceedings(DBLP:conf/its/2002, editor = "Stefano A. Cerri and Guy Gouard{\`e}res and F{\'a}bio Paragua\c {c}u", year = "2002", title = "Intelligent Tutoring Systems, 6th International Conference, ITS 2002, Biarritz, France and San Sebastian, Spain, June 2-7, 2002, Proceedings", series = "Lecture Notes in Computer Science", volume = "2363", publisher = "Springer", url = "http://dx.doi.org/10.1007/3-540-47987-2", ) @inproceedings(CheikhrouhouSorge00pds, author = "Lassaad Cheikhrouhou and Volker Sorge", year = "2000", title = "PDS -- A Three-Dimensional Data Structure for Proof Plans", booktitle = "Proceedings of the International Conference on Artificial and Computational Intelligence For Decision, Control and Automation In Engineering and Industrial Applications (ACIDCA) 2000", ) @article(Chi94elicitingself-explanations, author = "Michelene T. H. Chi and Nicholas De Leeuw and Mei hung Chiu and Christian Lavancher", year = "1994", title = "Eliciting self-explanations improves understanding", journal = "Cognitive Science", volume = "18", pages = "439--477", url = "http://dx.doi.org/10.1207/s15516709cog1803_3", ) @inproceedings(Claessen03newtechniques, author = "Koen Claessen and Niklas Sörensson", year = "2003", title = "New Techniques that Improve MACE-style Finite Model Finding", booktitle = "Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications", ) @incollection(Corbett2001, author = "Albert Corbett", year = "2001", title = "Cognitive Computer Tutors: Solving the Two-Sigma Problem", editor = "Mathias Bauer and Piotr Gmytrasiewicz and Julita Vassileva", booktitle = "User Modeling 2001", series = "Lecture Notes in Computer Science", volume = "2109", publisher = "Springer Berlin / Heidelberg", pages = "137--147", url = "http://dx.doi.org/10.1007/3-540-44566-8_14", ) @inproceedings(DBLP:conf/types/Corbineau07, author = "Pierre Corbineau", year = "2007", title = "A Declarative Language for the Coq Proof Assistant", editor = "Marino Miculan and Ivan Scagnetto and Furio Honsell", booktitle = "Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers", series = "Lecture Notes in Computer Science", volume = "4941", publisher = "Springer", pages = "69--84", url = "http://dx.doi.org/10.1007/978-3-540-68103-8_5", ) @inproceedings(hiproofs2006, author = "Ewen Denney and John Power and Konstantinos Tourlas", year = "2006", title = "Hiproofs: A Hierarchical Notion of Proof Tree", booktitle = "Proc. of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI), Birmingham, UK, May 18-21, 2005", series = "ENTCS", volume = "155", publisher = "Elsevier", pages = "341--359", url = "http://dx.doi.org/10.1016/j.entcs.2005.11.063", ) @article(DBLP:journals/entcs/DennisJP06, author = "Louise A. Dennis and Mateja Jamnik and Martin Pollet", year = "2006", title = "On the Comparison of Proof Planning Systems: lambdaCLAM, OMEGA and IsaPlanner", journal = "Electr. Notes Theor. Comput. Sci.", volume = "151", number = "1", pages = "93--110", url = "http://dx.doi.org/10.1016/j.entcs.2005.11.025", ) @phdthesis(dietrich2011, author = "Dominik Dietrich", year = "2010", title = "Assertion Level Proof Planning with Compiled Strategies", school = "Saarland University", ) @article(J20, author = "Dominik Dietrich and Mark Buckley", year = "2008", title = "Verification of Human-level Proof Steps in Mathematics Education", journal = "Teaching Mathematics and Computer Science", volume = "6", number = "2", pages = "345--362", ) @article(crystal-JAL, author = "Dominik Dietrich and Ewaryst Schulz", year = "2009", title = "Integrating Structured Queries into a Tactic Language", journal = "JAL - Special issue on Programming Languages and Mechanized Mathematics Systems", url = "http://dx.doi.org/10.1007/s10817-009-9138-5", ) @book(Ge-69-a, author = "Gerhard Gentzen", year = "1969", title = "{The Collected Papers of Gerhard Gentzen (1934-1938)}", publisher = "Edited by Szabo, M. E., North Holland", address = "Amsterdam", ) @misc(GeoGebra, author = "GeoGebra", year = "2008", title = "Dynamische Mathematiksoftware", howpublished = "http://www.geogebra.org", note = "Accessed December 5th, 2011.", ) @inproceedings(Gertner98proceduralhelp, author = "Abigail S. Gertner and Cristina Conati and Kurt Vanlehn", year = "1998", title = "Procedural help in Andes: Generating hints using a Bayesian network student", booktitle = "Proceedings of the 15th National Conference on Artificial Intelligence", publisher = "AAAI Press", pages = "106--111", url = "http://www.aaai.org/Conferences/AAAI/aaai98.php", ) @inproceedings(DBLP:conf/amast/GrundyL97, author = "Jim Grundy and Thomas L{\r a}ngbacka", year = "1997", title = "Recording HOL Proofs in a Structured Browsable Format", editor = "Michael Johnson", booktitle = "Algebraic Methodology and Software Technology, 6th International Conference, AMAST '97, Sydney, Australia, December 13-17, 1997, Proceedings", series = "Lecture Notes in Computer Science", volume = "1349", publisher = "Springer", pages = "567--571", url = "http://dx.doi.org/10.1007/BFb0000500", ) @inproceedings(conf/its/HeffernanC04, author = "Neil T. Heffernan and Ethan A. Croteau", year = "2004", title = "Web-Based Evaluations Showing Differential Learning for Tutorial Strategies Employed by the Ms. Lindquist Tutor.", editor = "James C. Lester and Rosa Maria Vicari and Fábio Paraguaçu", booktitle = "Intelligent Tutoring Systems", series = "Lecture Notes in Computer Science", volume = "3220", publisher = "Springer", pages = "491--500", url = "http://dx.doi.org/10.1007/978-3-540-30139-4_46", ) @inproceedings(huang94reconstructing, author = "Xiaorong Huang", year = "1994", title = "Reconstructing Proofs at the Assertion Level", editor = "Alan Bundy", booktitle = "Proc.\ 12th CADE", publisher = "Springer-Verlag", pages = "738--752", ) @book(Hu-96-a, author = "Xiaorong Huang", year = "1996", title = "Human Oriented Proof Presentation: A Reconstructive Approach", series = "DISKI", volume = "112", publisher = "Infix", address = "Sankt Augustin, Germany", ) @inproceedings(Kaliszyk07, author = "Cezary Kaliszyk and Freek Wiedijk and Maxim Hendriks and Femke van Raamsdonk", year = "2007", title = "{Teaching logic using a state-of-the-art proof assistant}", editor = "H. Geuvers and P. Courtieu", booktitle = "Proc.~of the International Workshop on Proof Assistants and Types in Education", pages = "33--48", ) @article(kelley1984, author = "John F. Kelley", year = "1984", title = "An iterative design methodology for user-friendly natural language office information applications", journal = "ACM Trans. Inf. Syst.", volume = "2", number = "1", pages = "26--41", url = "http://dx.doi.org/10.1145/357417.357420", ) @article(KoedingerAndAleven2007, author = "Kenneth R. Koedinger and Vincent Aleven", year = "2007", title = "Exploring the Assistance Dilemma in Experiments with Cognitive Tutors", journal = "Educational Psychology Review", volume = "19", pages = "239–--264", url = "http://dx.doi.org/10.1007/s10648-007-9049-0", ) @incollection(koedinger1993, author = "Kenneth R. Koedinger and John R. Anderson", year = "1993", title = "Reifying implicit planning in geometry: Guidelines for model-based intelligent tutoring system design", editor = "S. P. Lajoie and S. J. Derry", booktitle = "Computers as cognitive tools", publisher = "Erlbaum", address = "Hillsdale, NJ", pages = "15--46", ) @proceedings(DBLP:conf/mkm/2005, editor = "Michael Kohlhase", year = "2006", title = "Mathematical Knowledge Management, 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers", series = "Lecture Notes in Computer Science", volume = "3863", publisher = "Springer", url = "http://dx.doi.org/10.1007/11618027", ) @article(Lamport93howto, author = "Leslie Lamport", year = "1995", title = "How to write a proof", journal = "American Mathematical Monthly", volume = "102", number = "7", pages = "600--608", url = "http://dx.doi.org/10.2307/2974556", ) @proceedings(DBLP:conf/aied/2005, editor = "Chee-Kit Looi and Gordon I. McCalla and Bert Bredeweg and Joost Breuker", year = "2005", title = "Artificial Intelligence in Education - Supporting Learning through Intelligent and Socially Informed Technology, Proceedings of the 12th International Conference on Artificial Intelligence in Education, AIED 2005, July 18-22, 2005, Amsterdam, The Netherlands", series = "Frontiers in Artificial Intelligence and Applications", volume = "125", publisher = "IOS Press", ) @inproceedings(DBLP:conf/aied/MatsudaV05, author = "Noboru Matsuda and Kurt VanLehn", year = "2005", title = "Advanced Geometry Tutor: An intelligent tutor that teaches proof-writing with construction", editor = "\write \rebib { editor = "Looi",}", pages = "443--450", ) @article(DBLP:journals/corr/cs-SC-0310055, author = "William McCune", year = "2003", title = "Mace4 Reference Manual and Guide", journal = "CoRR", volume = "cs.SC/0310055", url = "http://arxiv.org/abs/cs.SC/0310055", ) @inproceedings(mclaren2008, author = "Bruce M. McLaren and Sung-Joo Lim and Kenneth R. Koedinger", year = "2008", title = "When and how often should worked examples be given to students? New results and a summary of the current state of research", booktitle = "Proceedings of the 30th Annual Conference of the Cognitive Science Society", organization = "Citeseer", pages = "2176--2181", ) @article(Activemath-01-a, author = "Erica Melis and Eric Andr\`es and Jochen B\"udenberger and Adrian Frischauf and George Goguadze and Paul Libbrecht and Martin Pollet and Carsten Ullrich", year = "2001", title = "ActiveMath: A Generic and Adaptive Web-Based Learning Environment", journal = "Artifical Intelligence in Education", volume = "12", number = "4", ) @article(Merrill_Reiser_Ranney_Trafton_1992, author = "Douglas C. Merrill and Brian J. Reiser and Michael Ranney and J. Gregory Trafton", year = "1992", title = "Effective Tutoring Techniques: A Comparison of Human Tutors and Intelligent Tutoring Systems", journal = "The Journal of the Learning Sciences", volume = "2", number = "3", pages = "277--305", url = "http://dx.doi.org/10.1207/s15327809jls0203_2", ) @inproceedings(Miller84, author = "Dale A. Miller", year = "1984", title = "Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs", editor = "Robert E. Shostak", booktitle = "7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings", series = "Lecture Notes in Computer Science", volume = "170", publisher = "Springer", pages = "375--393", url = "http://dx.doi.org/10.1007/BFb0047132", ) @book(NewellSimon72, author = "Allen. Newell and Herbert A. Simon", year = "1972", title = "Human Problem Solving", publisher = "Prentice Hall, Englewood Cliffs", ) @inproceedings(conf/its/NicaudBH02, author = "Jean-François Nicaud and Denis Bouhineau and Thomas Huguet", year = "2002", title = "The Aplusix-Editor: A New Kind of Software for the Learning of Algebra.", editor = "\write \rebib { editor = "Cerri",}", pages = "178--187", url = "http://dx.doi.org/10.1007/3-540-47987-2_22", ) @article(6551624, author = "Stellan Ohlsson", year = "1996", title = "{Learning from performance errors}", journal = "Psychological Review", volume = "103", pages = "241--262", url = "http://dx.doi.org/10.1037/0033-295X.103.2.241", ) @book(Ribenboim96, author = "Paulo Ribenboim", year = "1996", title = "The New Book of Prime Number Records", publisher = "Springer", ) @article(DBLP:journals/logcom/RobinsonS93, author = "Peter J. Robinson and John Staples", year = "1993", title = "Formalizing a Hierarchical Structure of Practical Mathematical Reasoning", journal = "J. Log. Comput.", volume = "3", number = "1", pages = "47--61", url = "http://dx.doi.org/10.1093/logcom/3.1.47", ) @inproceedings(Rose01acomparative, author = "Carolyn Penstein Ros\'{e} and Johanna D. Moore and Kurt Vanlehn and David Allbritton", year = "2001", title = "A comparative evaluation of socratic versus didactic tutoring", booktitle = "Society, University of Edinburgh", pages = "869--874", ) @book(marvinAKA2010, author = "Marvin Schiller", year = "2011", title = "Granularity Analysis for Tutoring Mathematical Proofs", publisher = "AKA Verlag", address = "Heidelberg", ) @inproceedings(lpar2006, author = "Marvin Schiller and Christoph Benzm\"{u}ller and Ann Van de Veire", year = "2006", title = "Judging Granularity for Automated Mathematics Teaching", booktitle = "LPAR 2006 Short Papers Proceedings", address = "Phnom Pehn, Cambodia", ) @article(DBLP:journals/igpl/Sieg07, author = "Wilfried Sieg", year = "2007", title = "The {AProS} Project: Strategic Thinking {\&} Computational Logic", journal = "Logic Journal of the IGPL", volume = "15", number = "4", pages = "359--368", url = "http://dx.doi.org/10.1093/jigpal/jzm026", ) @article(SiegScheines94, author = "Wilfried Sieg and Richard Scheines", year = "1994", title = "{Computer Environments for Proof Construction}", journal = "Interactive Learning Environments", volume = "4", number = "2", pages = "159--169", url = "http://dx.doi.org/10.1080/1049482940040203", ) @book(Solow05, author = "Daniel Solow", year = "2005", title = "How to read and do proofs", publisher = "John Wiley and Sons", ) @article(SommerNuckols04, author = "Richard Sommer and Gregory Nuckols", year = "2004", title = "{A Proof Environment for Teaching Mathematics}", journal = "Journal of Automated Reasoning", volume = "32", number = "3", pages = "227--258", url = "http://dx.doi.org/10.1007/s10817-004-5097-z", ) @inproceedings(DBLP:conf/its/SuraweeraM02, author = "Pramuditha Suraweera and Antonija Mitrovic", year = "2002", title = "KERMIT: A Constraint-Based Tutor for Database Modeling", editor = "\write \rebib { editor = "Cerri",}", pages = "377--387", url = "http://dx.doi.org/10.1007/3-540-47987-2_41", ) @inproceedings(Microsoft_threetactic, author = "Don Syme", year = "1999", title = "Three Tactic Theorem Proving", editor = "\write \rebib { editor = "Bertot",}", pages = "203--220", url = "http://dx.doi.org/10.1007/3-540-48256-3_14", ) @techreport(UCAM-CL-TR-416, author = "Donald Syme", year = "1997", title = "{DECLARE: a prototype declarative proof system for higher order logic}", type = "Technical Report", number = "UCAM-CL-TR-416", institution = "University of Cambridge", ) @inproceedings(trgalova2009, author = "Jana Trgalova and Hamid Chaachoua", year = "2009", title = "Automatic analysis of proof in a computer-based environment", editor = "F.-L. Lin and F.-J. Hsieh and G. Hanna and M. de Villiers", booktitle = "Proof and Proving in Mathematics Education, ICMI'19: Proceedings of the 19th International Conference on Mathematics Instruction, Taipei, Taiwan, May 10-15, 2009", volume = "1", pages = "226--231", ) @phdthesis(dimitraDiss, author = "Dimitra Tsovaltzi", year = "2010", title = "{MENON} - Automating a Socratic Teaching Model for Mathematical Proofs", type = "Phd thesis", school = "Universit\"{a}t des Saarlandes", address = "Saarbr\"ucken, Germany", ) @article(DBLP:journals/aiedu/VanLehn06, author = "Kurt VanLehn", year = "2006", title = "The Behavior of Tutoring Systems", journal = "I. J. Artificial Intelligence in Education", volume = "16", number = "3", pages = "227--265", url = "http://iospress.metapress.com/content/al6r85mm7c6qf7dr/", ) @article(vanlehn2011relative, author = "Kurt VanLehn", year = "2011", title = "The Relative Effectiveness of Human Tutoring, Intelligent Tutoring Systems, and Other Tutoring Systems", journal = "Educational Psychologist", volume = "46", number = "4", pages = "197–221", url = "http://dx.doi.org/10.1080/00461520.2011.611369", ) @article(DBLP:journals/aiedu/VanLehnLSSSTTWW05, author = "Kurt VanLehn and Collin Lynch and Kay G. Schulze and Joel A. Shapiro and Robert Shelby and Linwood Taylor and Donald Treacy and Anders Weinstein and Mary Wintersgill", year = "2005", title = "The Andes Physics Tutoring System: Lessons Learned", journal = "I. J. Artificial Intelligence in Education", volume = "15", number = "3", pages = "147--204", url = "http://iospress.metapress.com/content/4qh80ubfdft0g4yr/", ) @inproceedings(DBLP:conf/tphol/Wenzel99, author = "Markus Wenzel", year = "1999", title = "Isar - A Generic Interpretative Approach to Readable Formal Proof Documents", editor = "\write \rebib { editor = "Bertot",}", pages = "167--184", url = "http://dx.doi.org/10.1007/3-540-48256-3_12", ) @inproceedings(Wiedijk02formalproof, author = "Freek Wiedijk", year = "2004", title = "Formal Proof Sketches", editor = "Mario Coppo Stefano Berardi and Ferruccio Damiani", booktitle = "Types for Proofs and Programs: Third International Workshop TYPES 2003", series = "LNCS", volume = "3085", publisher = "Springer", address = "Torino", pages = "378--393", url = "http://dx.doi.org/10.1007/978-3-540-24849-1_24", ) @incollection(springerlink:10.1007/978-3-540-89408-7_12, author = "Magdalena Wolska and Mark Buckley and Helmut Horacek and Ivana Kruijff-Korbayová and Manfred Pinkal", year = "2010", title = "Linguistic Processing in a Mathematics Tutoring System: Cooperative Input Interpretation and Dialogue Modelling", editor = "Matthew W. Crocker and Jörg Siekmann", booktitle = "Resource-Adaptive Cognitive Processes", series = "Cognitive Technologies", publisher = "Springer Berlin Heidelberg", pages = "267--289", url = "http://dx.doi.org/10.1007/978-3-540-89408-7_12", ) @book(Woolf2008, author = "Beverly Park Woolf", year = "2008", title = "Building intelligent interactive tutors: Student-centered strategies for revolutionizing e-learning", publisher = "Morgan Kaufmann", )