Boston University Libraries OpenBU
    JavaScript is disabled for your browser. Some features of this site may not work without it.
    View Item 
    •   OpenBU
    • College of Arts and Sciences
    • Computer Science
    • CAS: Computer Science: Technical Reports
    • View Item
    •   OpenBU
    • College of Arts and Sciences
    • Computer Science
    • CAS: Computer Science: Technical Reports
    • View Item

    Accessible integrated formal reasoning environments in classroom instruction of mathematics

    Thumbnail
    Date Issued
    2012-12-10
    Author(s)
    Lapets, Andrei
    Share to FacebookShare to TwitterShare by Email
    Export Citation
    Download to BibTex
    Download to EndNote/RefMan (RIS)
    Metadata
    Show full item record
    Permanent Link
    https://hdl.handle.net/2144/11403
    Citation (published version)
    Lapets, Andrei. "Accessible Integrated Formal Reasoning Environments in Classroom Instruction of Mathematics", Technical Report BUCS-TR-2012-015, Computer Science Department, Boston University, December 10, 2012. [Available from: http://hdl.handle.net/2144/11403]
    Abstract
    Computer science researchers in the programming languages and formal verification communities, among others, have produced a variety of automated assistance and verification tools and techniques for formal reasoning. While there have been notable successes in utilizing these tools on the development of safe and secure software and hardware, these leading-edge advances remain largely underutilized by large populations of potential users that may benefit from them; among these are instructors and students engaged in the undergraduate-level instruction and study of mathematics. Building on earlier work in assembling and evaluating accessible formal verification tools for research and classroom instruction, we have assembled an interactive web-based integrated formal reasoning environment that incorporates several standard techniques developed by the programming languages and formal verification communities. This environment can run entirely within a standard web browser, and provides interactive and instant verification feedback about logical validity, as well as an interactive, exhaustive list of all inferred properties for a given formal argument input. The environment provides an explicit library of logical definitions and formulas that instructors can curate and students can utilize to complete assignments; these formulas can be browsed and filtered by students within the environment. The underlying infrastructure also allows instructors to assemble lecture notes and assignments containing within them formal arguments (including both complete examples and problems to be solved by students) that can be automatically loaded into the environment with one click. This environment has been utilized within the classroom for an undergraduate-level course in linear algebra, both by the instructor in presenting examples during lectures, and by students when completing homework assignments.
    Collections
    • CAS: Computer Science: Technical Reports [586]


    Boston University
    Contact Us | Send Feedback | Help
     

     

    Browse

    All of OpenBUCommunities & CollectionsIssue DateAuthorsTitlesSubjectsThis CollectionIssue DateAuthorsTitlesSubjects

    Deposit Materials

    LoginNon-BU Registration

    Statistics

    Most Popular ItemsStatistics by CountryMost Popular Authors

    Boston University
    Contact Us | Send Feedback | Help