Without Loss of Generality

DOI10.1007/978-3-642-03359-9_3zbMath1252.68254OpenAlexW1528908721MaRDI QIDQ3183516

No author found.

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)

Related Items (14)

A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ Lyndon words formalized in Isabelle/HOL ⋮ SYMMETRIES IN MODAL LOGICS ⋮ The HOL Light theory of Euclidean space ⋮ What does ``without loss of generality mean, and how do we detect it ⋮ Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1 ⋮ Formalization of the Poincaré disc model of hyperbolic 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 ⋮ Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL ⋮ Formula simplification via invariance detection by algebraically indexed types ⋮ Relevance-Sensitive Truth-Trees ⋮ Formalizing complex plane geometry

Uses Software

• ML
• HOL
• Jordan

Cites Work

• Unnamed Item
• Some new results on decidability for elementary algebra and geometry
• Edinburgh LCF. A mechanized logic of computation
• The Jordan Curve Theorem, Formally and Informally
• Theorem Proving in Higher Order Logics

This page was built for publication: Without Loss of Generality