Automated Reasoning and Mathematics

Essays in Memory of William W. McCune

Häftad, Engelska, 2013

649 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt för medlemmar vid köp för minst 249 kr.

The topics covered are: strategies, indexing, superposition-based theorem proving, model building, application of automated reasoning to mathematics, as well as to program verification, data mining, and computer formalized mathematics.

Produktinformation

Utgivningsdatum2013-03-19
Mått155 x 235 x 16 mm
Vikt429 g
FormatHäftad
SpråkEngelska
SerieLecture Notes in Computer Science
Antal sidor259
Upplaga2013
FörlagSpringer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN9783642366741

Tillhör följande kategorier

Systemvetenskap och AI inom Data och it
Artificiell intelligens inom Data och it

The Legacy of a Great Researcher.- The Strategy Challenge in SMT Solving.- Simple and Efficient Clause Subsumption with Feature Vector Indexing.- Superposition for Bounded Domains.- MACE4 and SEM: A Comparison of Finite Model Generators.- Group Embedding of the Projective Plane PG(2, 3).- A Geometric Procedure with Prover9.- Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction.- (Dual) Hoops Have Unique Halving.- Gibbard’s Collapse Theorem for the Indicative Conditional: An Axiomatic Approach.- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants.- Toward a Procedure for Data Mining Proofs.- Theorem Proving in Large Formal Mathematics as an Emerging AI Field. The Strategy Challenge in SMT Solving.- Simple and Efficient Clause Subsumption with Feature Vector Indexing.- Superposition for Bounded Domains.- MACE4 and SEM: A Comparison of Finite Model Generators.- Group Embedding of the Projective Plane PG(2, 3).- A Geometric Procedure with Prover9.- Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction.- (Dual) Hoops Have Unique Halving.- Gibbard’s Collapse Theorem for the Indicative Conditional: An Axiomatic Approach.- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants.- Toward a Procedure for Data Mining Proofs.- Theorem Proving in Large Formal Mathematics as an Emerging AI Field.