Automated Reasoning and Mathematics

Essays in Memory of William W. McCune

AvMaria Paola Bonacina,Mark E. Stickel

Häftad, Engelska, 2013

Del i serien Lecture Notes in Computer Science

507 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Beskrivning

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

Utgivningsdatum:2013-03-19
Mått:155 x 235 x 16 mm
Vikt:429 g
Format:Häftad
Språk:Engelska
Serie:Lecture Notes in Computer Science
Antal sidor:259
Upplaga:2013
Förlag:Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN:9783642366741

Utforska kategorier

Systemvetenskap och AI inom Data och IT
Artificiell intelligens inom Data och IT

Innehållsförteckning

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.