Loading...
Please wait, while we are loading the content...
Similar Documents
On locally minimal Nullstellensatz proofs
| Content Provider | ACM Digital Library |
|---|---|
| Author | de Moura, Leonardo Passmore, Grant Olney |
| Abstract | Hilbert's weak Nullstellensatz guarantees the existence of algebraic proof objects certifying the unsatisfiability of systems of polynomial equations not satisfiable over any algebraically closed field. Such proof objects take the form of ideal membership identities and can be found algorithmically using Gröbner bases and cofactor-based linear algebra techniques. However, these proof objects may contain redundant information: a proper subset of the equational assumptions used in these proofs may be sufficient to derive the unsatisfiability of the original polynomial system. For using Nullstellensatz techniques in SMT-based decision methods, a minimal proof object is often desired. With this in mind, we introduce a notion of locally minimal Nullstellensatz proofs and give ideal-theoretic algorithms for their construction. |
| Starting Page | 35 |
| Ending Page | 42 |
| Page Count | 8 |
| File Format | |
| ISBN | 9781605584843 |
| DOI | 10.1145/1670412.1670418 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2009-08-02 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Gröbner bases Automated reasoning Decision procedures Formal proofs Non-linear arithmetic Smt Satisfiability modulo theories Computer algebra |
| Content Type | Text |
| Resource Type | Article |
