Milestones from the Pure Lisp Theorem Prover to ACL2 (Q2280212): Difference between revisions

From MaRDI portal
Importer (talk | contribs)
Created a new Item
 
ReferenceBot (talk | contribs)
Changed an Item
 
(19 intermediate revisions by 5 users not shown)
Property / author
 
Property / author: J. Strother Moore / rank
Normal rank
 
Property / author
 
Property / author: J. Strother Moore / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: ACL2 / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Isabelle/HOL / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: LCF / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: DefunT / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: TXDT / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Coq / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: ML / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: PVS / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: HOL / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: LISP / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Quicksort / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: NQTHM / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Milawa / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Jitawa / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1007/s00165-019-00490-3 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W2964806919 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A man-machine theorem-proving system / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4016540 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Splitting and reduction heuristics in automatic theorem proving / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5663380 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proving Theorems about LISP Functions / rank
 
Normal rank
Property / cites work
 
Property / cites work: A fast string searching algorithm / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3894958 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3932277 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The addition of bounded quantification and partial functions to a computational logic and its theorem prover / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4040283 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3835049 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The ACL2 Sedan Theorem Proving System / rank
 
Normal rank
Property / cites work
 
Property / cites work: Efficient certified RAT verification / rank
 
Normal rank
Property / cites work
 
Property / cites work: The reflective Milawa theorem prover is sound (down to the machine code that runs it) / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5610986 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5287513 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2754047 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Efficient, verified checking of propositional proofs / rank
 
Normal rank
Property / cites work
 
Property / cites work: An extension of the Boyer-Moore theorem prover to support first-order quantification / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5670164 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Linear resolution with selection function / rank
 
Normal rank
Property / cites work
 
Property / cites work: Limited second-order functionality in a first-order setting / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3154457 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5601829 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3857731 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Automated Deduction – CADE-19 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Simplification by Cooperating Decision Procedures / rank
 
Normal rank
Property / cites work
 
Property / cites work: Isabelle/HOL. A proof assistant for higher-order logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: A Machine-Oriented Logic Based on the Resolution Principle / rank
 
Normal rank
Property / cites work
 
Property / cites work: A Practical Decision Procedure for Arithmetic with Function Symbols / rank
 
Normal rank
Property / cites work
 
Property / cites work: Toward Mechanical Mathematics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Prolegomena to a theory of mechanized formal reasoning / rank
 
Normal rank
links / mardi / namelinks / mardi / name
 

Latest revision as of 06:38, 21 July 2024

scientific article
Language Label Description Also known as
English
Milestones from the Pure Lisp Theorem Prover to ACL2
scientific article

    Statements

    Milestones from the Pure Lisp Theorem Prover to ACL2 (English)
    0 references
    18 December 2019
    0 references
    theorem proving
    0 references
    hardware
    0 references
    software
    0 references
    verification
    0 references
    functional programming
    0 references
    Lisp
    0 references
    induction
    0 references
    rewriting
    0 references
    reflection
    0 references
    decision procedures
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers