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

• Edinburgh LCF. A mechanized logic of computation
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• 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

(21)

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

Describes a project that uses

Uses Software

• ML
• Jordan
• HOL

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)