Formula simplification via invariance detection by algebraically indexed types

DOI10.1007/978-3-031-10769-6_24MaRDI QIDQ2104529zbMATH OpenOpenAlexFDO

Authors Takuya Matsuzaki, Tomohiro Fujita

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-10769-6_24

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver
• Abstraction and invariance for algebraically indexed types
• Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
• CDCLSym: introducing effective symmetry breaking in SAT solving
• Formula Simplification for Real Quantifier Elimination Using Geometric Invariance
• Homomorphisms of conjunctive normal forms.
• scientific article; zbMATH DE number 1612537 (Why is no real title available?)
• Improved static symmetry breaking for SAT
• Race against the teens -- benchmarking mechanized math on pre-university problems
• Short proofs for tricky formulas
• The complexity of quantifier elimination and cylindrical algebraic decomposition
• Tractability of cut-free Gentzen type propositional calculus with permutation inference
• What does ``without loss of generality mean, and how do we detect it
• Without Loss of Generality

Describes a project that uses

Uses Software

• CDCLSym
• SymChaff

This page was built for publication: Formula simplification via invariance detection by algebraically indexed types

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