Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Branch: master
Commits on Aug 15, 2015
  1. books/bookvol10.* extract code for COQ proof system

    authored
    Goal: Proving Axiom Correct
    
    Collect all of the functions in the categories, domains, and packages
    into obj/sys/proofs/coq.v
Commits on Aug 4, 2015
  1. buglist bug 7303: Duplicate signature in )show ALIST

    authored
    Goal: Proving Axiom Correct
    
    This signature appears to be a duplicate in the )show command.
    The reason is unclear and is marked as a bug.
  2. books/bookvol10.* add COQ stanzas

    authored
    Goal: Proving Axiom Correct
    
    Stanzas were added to the algebra that contain the executable code
    with associated signatures. These stanzas are automatically extracted
    to the obj/sys/proofs/coq.v file. This file is piped through coqtop
    to run the proofs.
    
    Building stanzas is not complete but is (maybe) sufficient to construct
    a first proof.
  3. books/bookvol10.* add COQ stanzas

    authored
    Goal: Proving Axiom Correct
    
    Stanzas were added to the algebra that contain the executable code
    with associated signatures. These stanzas are automatically extracted
    to the obj/sys/proofs/coq.v file. This file is piped through coqtop
    to run the proofs.
    
    Building stanzas is not complete but is (maybe) sufficient to construct
    a first proof.
Commits on Jul 31, 2015
  1. buglist: add TODO for erf-related conversion to Float

    authored
    Goal: Add New Math Functionality
    
    Extending the mathematical ability of Axiom is a primary goal.
    It seems these ought to work so add them to the todo list.
    
    =========================================================================
    todo 338: Convert to Float fails
    
    (1) -> eval(integrate(x*exp(-(x-u)^2/2)/(sqrt(2*%pi)),x=a..%plusInfinity),[a=1,u=0.5])
    
       (1)  - 0.25 erf(0.3535533905 932737622) + 0.6020653267 6429947778
                                                          Type: Expression(Float)
    (2) -> eval(integrate(x*exp(-(x-u)^2/2)/(sqrt(2*%pi)),x=a..%plusInfinity),[a=1,u=0.5])::Float
    
       Cannot convert from type Expression(Float) to Float for value
       - 0.25 erf(0.3535533905 932737622) + 0.6020653267 6429947778
    
    =========================================================================
    todo 337: erf does not evaluate
    
    (2) -> - 0.25* erf(0.3535533905932737622) + 0.60206532676429947778
    
       (2)  - 0.25 erf(0.3535533905 932737622) + 0.6020653267 6429947778
                                                          Type: Expression(Float)
    (3) -> erf(0.3535533905932737622)
    
       (3)  erf(0.3535533905 932737622)
Commits on Jul 29, 2015
  1. books/bookvol13 Add mathematics for GCD proof

    authored
    Goal: Prove Axiom correct
    
    Buchberger presents a proof of the GCD algorithm.
Commits on Jul 18, 2015
  1. books/bookvolbib: Add program proof papers

    authored
    Goal: Prove Axiom correct
    
    Several papers related to proving algorithms (Buchberger's, GCD,
    and Cylindrical Algebraic Decomposition) were added.
Commits on Jul 16, 2015
  1. Makefile: extract and run proof code automatically

    authored
    Goal: Prove Axiom correct
    
    If the command line include "COQ=coq" then the system extracts the
    'coq' chunk from the books and run coq proof code automatically.
  2. Makefile: extract and run proof code automatically

    authored
    Goal: Prove Axiom correct
    
    If the command line include "ACL2=acl2" then the system extracts the
    'acl2' chunk from the books and run acl2 proof code automatically.
Commits on Jul 15, 2015
  1. books/bookvol5: Use ACL2 to prove isWrapped function

    authored
    Goal: Prove Axiom correct
    
    This is the first example of using ACL2 against the Axiom
    common lisp code to prove the function correct. The signature
    for isWrapped is
    
       isWrapped: t -> (or t nil)
    
    It is a predicate that takes any argument and returns either t or nil.
Commits on Jul 12, 2015
  1. src/interp/i-coerce.lisp fix use of eqType assignment

    authored
    Goal: Clean code
    
    The eqType function disappears during compile so that
    t := eqType t turns into t := t. The following code becomes a nop
    and has been removed.
Commits on Jul 11, 2015
  1. readme: Add Laurent Thery to credits (COQ Proof)

    authored
    Goal: Maintaining correct credit list
  2. books/bookvol5 merge functions used from i-coerce

    authored
    Goal: Literate Axiom
    
    Every function in src/input/i-coerce.lisp that was referenced
    in bookvol5 was moved and rewritten from i-coerce to bookvol5.
  3. books/bookvol10.3, src/input/intlf,series minor test fixes

    authored
    Goal: Clean Axiom Test Suite
    
    Minor test fixes.
  4. books/bookvol13 more work on proving Axiom

    authored
    Goal: Axiom proven correct
    
    Add references for proofs in COQ using OCaml and Common Lisp.
    Obtained permission to use Theiry work.
Commits on Jul 2, 2015
  1. src/input/*.input.pamphlet

    authored
    Goal: clean test suite
    
    Minor fixes were made to bookvol10.4, cachedf, clements, polycoer, and
    tuplebug to clean up test cases.
Commits on Jun 21, 2015
  1. src/interp/interop.lisp merge and purge code

    authored
    Goal: move toward Literate
    
    The interop.lisp file contained code to handle a prior representation
    of Scratchpad code. That representation no longer exists so compiling
    the code was a waste of time. Functions that checked for the prior
    representation always returned false, wasting runtime.  Some of the
    code was used elsewhere and it was moved or merged into the interpreter
    book (5), the rest was deleted. The interop.lisp file was removed.
Commits on Jun 18, 2015
  1. src/interp/i-code.lisp common lisp cleanup

    authored
    Goal: move toward Common Lisp, rewrite compiler output
  2. src/interp/br-con.lisp common lisp cleanup

    authored
    Goal: move toward Common Lisp, rewrite compiler output
Commits on Jun 3, 2015
  1. src/interp/vmlisp.lisp remove lispelt

    authored
    Goal: Remove MACLISP, move toward Common Lisp
  2. src/interp/vmlisp.lisp remove lasttail

    authored
    Goal: Remove MACLISP, move toward Common Lisp
Commits on May 27, 2015
  1. books/bookvol5 move PLACEP VMREAD to Algebra support section

    authored
    Goal: Collect functions that directly support algebra in one place
    
    placep and vmread are used in File. They have been moved to the
    proper section in the interpreter from vmlisp.
Commits on May 26, 2015
  1. src/interp/vmlisp.lisp remove KAR, KDR, KAAR, KADR macros

    authored
    move closer to common lisp.
Commits on May 20, 2015
  1. books/bookvolbib add Thie15 reference

    authored
    @misc{Thie15,
      author = "Thiery, Nicolas M.",
      title = "Open Digital Research Environment Toolkit for the Advancement of Mathematics",
      year = "2015",
      url = "http://opendreamkit.org",
      paper = "Thie15.pdf",
      abstract =
       "OpenDreamKit will deliver a flexible toolkit enabling research groups
        to set up Virtual Research Environments, customised to meet the varied
        needs of research projects in pure mathematics and applications, and
        supporting the full research life-cycle from exploration, through
        proof and publication, to archival and sharing of data and code.
    
        OpenDreamKit will be built out of a sustainable ecosystem of
        community-developed open software, databases, and ser- vices,
        including popular tools such as LINBOX, MPIR, SAGE (sagemath.org),
        GAP, PARI/GP, LMFDB, and SINGULAR. We will extend the JUPYTER Notebook
        environment to provide a flexible user interface. By improving and
        unifying existing build- ing blocks, OpenDreamKit will maximise both
        sustainability and impact, with beneficiaries extending to scientific
        computing, physics, chemistry, biology and more, and including
        researchers, teachers, and industrial practitioners.
    
        We will define a novel component-based VRE architecture and adapt
        existing mathematical software, databases, and user interface
        components to work well within it on varied platforms. Interfaces to
        standard HPC and grid services will be built in. Our architecture will
        be informed by recent research into the sociology of mathematical
        collaboration, so as to properly support actual research practice. The
        ease of set up, adaptability and global impact will be demonstrated in
        a variety of demonstrator VREs.
    
        We will ourselves study the social challenges associated with
        large-scale open source code development and publications based on
        executable documents, to ensure sustainability.
    
        OpenDreamKit will be conducted by a Europe-wide steered by demand
        collaboration, including leading mathematicians, computational
        researchers, and software developers with a long track record of
        delivering innovative open source software solutions for their
        respective communities. All produced code and tools will be open
        source."
    }
Commits on May 19, 2015
  1. src/interp/c-doc.lisp merge c-doc functions, removed

    authored
    The functions are all in bookvol9 (compiler).
    This file was merged and removed.
  2. src/interp/vmlisp.lisp rewrite character handling functions

    authored
    Use common lisp native forms.
  3. src/interp/vmlisp.lisp remove define-macro

    authored
    No longer needed.
  4. Makefile clean up dangling files

    authored
    There were some files that escaped the 'clean' step.
  5. src/interp/vmlisp.lisp remove |equal|, evalandfileactq

    authored
    use common lisp forms
Commits on May 18, 2015
  1. src/interp/vmlisp.lisp remove spaddifference

    authored
    rename spaddifference to -, i.e. standard common lisp name
Commits on May 16, 2015
  1. src/interp/vmlisp.lisp revert from broken version

    authored
    Over-optimization of this file caused build breakage. Revert
    the version until fixed.
Commits on May 8, 2015
  1. books/bookvolbib add Robe15 reference

    authored
    @misc{Robe15,
     author = "Roberts, Siobhan",
     title = "In Mathematics, Mistakes Aren't What They Used To Be",
     year = 2015,
     url = "http://nautil.us/issue/24/error/In-mathematics-mistakes-arent-what-they-used-to-be"
Commits on May 5, 2015
  1. books/bookvol13 add Kama15 reference

    authored
    Add Kama15 to the Axiom Proof book.
  2. books/bookvolbib add Kama14 to paper collection

    authored
    @misc{Kama15,
      author = "Kamareddine, Fairouz and Wells, Joe and Zengler, Christoph and
                Barendregt, Henk",
      title = "Computerising Mathematical Text",
      url =
    "http://repository.ubn.ru.nl/bitstream/handle/2066/134655/134655.pdf?sequence=1",
      paper = "Kama15.pdf",
      abstract =
        "Mathematical texts can be computerised in many ways that capture
        differing amounts of the mathematical meaning. At one end, there is
        document imag- ing, which captures the arrangement of black marks on
        paper, while at the other end there are proof assistants (e.g., Mizar,
        Isabelle, Coq, etc.), which capture the full mathematical meaning and
        have proofs expressed in a formal foundation of mathematics. In
        between, there are computer typesetting systems (e.g., LATEX and
        Presentation MathML) and semantically oriented systems (e.g., Content
        MathML, OpenMath, OMDoc, etc.). In this paper we advocate a style of
        computerisation of mathematical texts which is flexible enough to
        connect the different approaches to computerisation, which allows
        various degrees of formalisation, and which is compatible with
        different logical frameworks (e.g., set theory, category theory, type
        theory, etc.) and proof systems. The basic idea is to allow a
        man-machine collaboration which weaves human input with machine
        computation at every step in the way. We propose that the huge step
        from informal mathematics to fully formalised mathematics be divided
        into smaller steps, each of which is a fully developed method in which
        human input is minimal.  Let us consider the following two questions:
        \begin{enumerate}
        \item What is the relationship between the logical foundations of
        mathematical reasoning and the actual practice of mathematicians?
        \item In what ways can computers support the development and
        communication of mathematical knowledge?
        \end{enumerate}"
    }
Something went wrong with that request. Please try again.