Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (Q2102946): Difference between revisions

From MaRDI portal
← Older edit
‎Changed an Item
Import241208061232 (talk | contribs)
1,083,878 edits
Normalize DOI.
 
(10 intermediate revisions by 5 users not shown)
Property / DOI
 
Property / DOI: 10.1007/s10817-022-09643-1 / rank
Normal rank
 
Property / describes a project that uses
 
Property / describes a project that uses: Isabelle/Isar / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Automath / 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: Isar / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: kepler98 / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Sledgehammer / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / Wikidata QID
 
Property / Wikidata QID: Q114689845 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W3195133477 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3367316 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A note on ‘Einstein's special relativity beyond the speed of light by James M. Hill and Barry J. Cox’ / rank
 
Normal rank
Property / cites work
 
Property / cites work: The significance of ptolemy's Almagest for its early readers / rank
 
Normal rank
Property / cites work
 
Property / cites work: From Tarski to Hilbert / rank
 
Normal rank
Property / cites work
 
Property / cites work: A system of axioms for Minkowski spacetime / rank
 
Normal rank
Property / cites work
 
Property / cites work: Selected papers on AUTOMATH, dedicated to N. G. de Bruijn / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5719494 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formalizing Ordinal Partition Relations Using Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4735709 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Orthogonality and spacetime geometry / rank
 
Normal rank
Property / cites work
 
Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank
 
Normal rank
Property / cites work
 
Property / cites work: Special Relativity in General Frames / rank
 
Normal rank
Property / cites work
 
Property / cites work: A formulation of the Kepler conjecture / rank
 
Normal rank
Property / cites work
 
Property / cites work: Without Loss of Generality / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3234138 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A potential foundation for emergent space-time / rank
 
Normal rank
Property / cites work
 
Property / cites work: Comprehending Isabelle/HOL’s Consistency / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Kepler Conjecture / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formalizing Projective Plane Geometry in Coq / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formalizing Hilbert’s Grundlagen in Isabelle/Isar / rank
 
Normal rank
Property / cites work
 
Property / cites work: Verisimilitude Redefined / rank
 
Normal rank
Property / cites work
 
Property / cites work: Mechanical Theorem Proving in Tarski’s Geometry / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4556039 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Term rewriting and beyond -- theorem proving in Isabelle / rank
 
Normal rank
Property / cites work
 
Property / cites work: From LCF to Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: Foundations of special relativity: Kinematic axioms for Minkowski space- time / rank
 
Normal rank
Property / cites work
 
Property / cites work: An axiomatic system for Minkowski space–time / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4373932 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A type-theoretical alternative to ISWIM, CUCH, OWHY / rank
 
Normal rank
Property / cites work
 
Property / cites work: An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time / rank
 
Normal rank
Property / cites work
 
Property / cites work: Using Isabelle/HOL to verify first-order relativity theory / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2784341 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Kinematic geometry; an axiomatic system for Minkowski space-time / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4781180 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3268764 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3263441 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5219926 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Isabelle Framework / rank
 
Normal rank
Property / DOI
 
Property / DOI: 10.1007/S10817-022-09643-1 / rank
 
Normal rank

Latest revision as of 01:50, 17 December 2024

scientific article
Language Label Description Also known as
English
Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
scientific article

    Statements

    title
    Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (English)
    0 references
    author
    Richard Schmoetten
    0 references
    Jake E. Palmer
    0 references
    Jacques D. Fleuriot
    0 references
    publication date
    12 December 2022
    0 references
    zbMATH Keywords
    Isabelle
    0 references
    relativity
    0 references
    Minkowski
    0 references
    synthetic geometry
    0 references
    describes a project that uses
    Isabelle
    0 references
    Archive Formal Proofs
    0 references
    Isabelle/Isar
    0 references
    Automath
    0 references
    Isabelle/HOL
    0 references
    Isar
    0 references
    kepler98
    0 references
    Sledgehammer
    0 references
    cites work
    Q3367316
    0 references
    From Tarski to Hilbert
    0 references
    Q5719494
    0 references
    Q4735709
    0 references
    Q3234138
    0 references
    The Kepler Conjecture
    0 references
    Q4556039
    0 references
    Q4373932
    0 references
    Q2784341
    0 references
    Q4781180
    0 references
    Q3268764
    0 references
    Q3263441
    0 references
    Q5219926
    0 references
    The Isabelle Framework
    0 references

    Identifiers

    zbMATH DE Number
    7632096
    0 references
    Wikidata QID
    Q114689845
    0 references
    OpenAlex ID
    W3195133477
    0 references
     
    Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Item:Q2102946&oldid=38880557"
    Powered by MediaWiki