Without Loss of Generality

DOI10.1007/978-3-642-03359-9_3MaRDI QIDQ3183516zbMATH OpenOpenAlexFDO

Authors

Publication date 20 October 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-03359-9_3

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• What does ``without loss of generality mean, and how do we detect it
• Symmetry as a method of proof
• The phenomenology of second-level inference: perfumes in the deductive garden
• scientific article; zbMATH DE number 4135936
• Why proof? What is a proof?

Cites work

• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Edinburgh LCF. A mechanized logic of computation
• Some new results on decidability for elementary algebra and geometry
• The Jordan Curve Theorem, Formally and Informally
• Theorem Proving in Higher Order Logics

Cited in

(19)

• Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
• Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
• Formula simplification via invariance detection by algebraically indexed types
• Lyndon words formalized in Isabelle/HOL
• Formalization of the Poincaré disc model of hyperbolic geometry
• A formal proof of the Kepler conjecture
• Formalization of Wu's simple method in Coq
• Formalizing complex plane geometry
• Towards automated proving in solid geometry
• Formalization of gyrovector spaces as models of hyperbolic geometry and special relativity
• Formalizing Pick's theorem in Isabelle/HOL
• Formalising geometric axioms for Minkowski spacetime and without-loss-of-generality theorems
• Spreads and packings of PG(3,2), formally!
• Relevance-Sensitive Truth-Trees
• The phenomenology of second-level inference: perfumes in the deductive garden
• The HOL Light theory of Euclidean space
• Symmetries in modal logics
• What does ``without loss of generality mean, and how do we detect it
• A formal proof of Pick's theorem

Describes a project that uses

Uses Software

• Jordan
• HOL
• ML

This page was built for publication: Without Loss of Generality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3183516)