國立虎尾科技大學 |

Automated Deduction – CADE 27 = 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings /

紀錄類型:	書目-語言資料,印刷品 : Monograph/item
正題名/作者:	Automated Deduction – CADE 27/ edited by Pascal Fontaine.
其他題名:	27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings /
其他作者:	Fontaine, Pascal.
面頁冊數:	XXIII, 582 p. 1901 illus., 56 illus. in color.online resource. :
Contained By:	Springer Nature eBook
標題:	Artificial intelligence. -
電子資源:	https://doi.org/10.1007/978-3-030-29436-6
ISBN:	9783030294366

Automated Deduction – CADE 27 = 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings /
Automated Deduction – CADE 2727th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings /[electronic resource] :edited by Pascal Fontaine. - 1st ed. 2019. - XXIII, 582 p. 1901 illus., 56 illus. in color.online resource. - Lecture Notes in Artificial Intelligence ;11716. - Lecture Notes in Artificial Intelligence ;9285.

Automated Reasoning for Security Protocols -- Computer Deduction and (Formal) Proofs in Mathematics -- From Counter-Model-based Quantifier Instantiation to Quantifier Elimination in SMT -- The CADE-27 ATP System Competition - CASC-27 -- Unification modulo Lists with Reverse - Relation with Certain Word Equations -- On the Width of Regular Classes of Finite Structures -- Extending SMT solvers to Higher-Order Logic -- Superposition with Lambdas -- Restricted Combinatory Unification -- dLi: Definite Descriptions in Differential Dynamic Logic -- SPASS-SATT { A CDCL(LA) Solver -- GRUNGE: A Grand Unified ATP Challenge -- Model Completeness, Covers and Superposition -- A Tableaux Calculus for Default Intuitionistic Logic -- NIL: Learning Nonlinear Interpolants -- ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E -- Towards Physical Hybrid Systems -- SCL -- Clause Learning from Simple Models -- Names are not just Sound and Smoke: Word Embeddings for Axiom Selection -- Computing Expected Runtimes for Constant Probability Programs -- Automatic Generation of Logical Models with AGES -- Automata Terms in a Lazy WSkS Decision Procedure -- Confluence by Critical Pair Analysis Revisited -- Composing Proof Terms -- Combining ProVerif and Automated Theorem Provers for Security Protocol Verification -- Towards Bit-Width-Independent Proofs in SMT Solvers -- On Invariant Synthesis for Parametric Systems -- The Aspect Calculus -- Uniform Substitution At One Fell Swoop -- A Formally Verified Abstract Account of Gödel's Incompleteness Theorems -- Old or Heavy? Decaying Gracefully with Age/Weight Shapes -- Induction in Saturation-Based Proof Search -- Faster, Higher, Stronger: E 2.3 -- Certified Equational Reasoning via Ordered Completion -- JGXYZ - An ATP System for Gap and Glut Logics -- GKC: a Reasoning System for Large Knowledge Bases -- Optimization Modulo the Theory of Floating-Point Numbers -- FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions. .

This book constitutes the proceeding of the 27th International Conference on Automated Deduction, CADE 27, held in Natal, Brazil, in August 2019. The 27 full papers and 7 system descriptions presented were carefully reviewed and selected from 65 submissions. CADE is the major forum for the presentation of research in all aspects of automated deduction, including foundations, applications, implementations, and practical experience. .

ISBN: 9783030294366

Standard No.: 10.1007/978-3-030-29436-6doiSubjects--Topical Terms:

559380
Artificial intelligence.

LC Class. No.: Q334-342

Dewey Class. No.: 006.3

Automated Deduction – CADE 27 = 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings /
LDR:03952nam a22004095i 4500 001 1007277
003 DE-He213
005 20200703084531.0
007 cr nn 008mamaa
008 210106s2019 gw | s |||| 0|eng d
020 $a 9783030294366 $9 978-3-030-29436-6
024 7 $a 10.1007/978-3-030-29436-6 $2 doi
035 $a 978-3-030-29436-6
050 4 $a Q334-342
072 7 $a UYQ $2 bicssc
072 7 $a COM004000 $2 bisacsh
072 7 $a UYQ $2 thema
082 0 4 $a 006.3 $2 23
245 1 0 $a Automated Deduction – CADE 27 $h [electronic resource] : $b 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings / $c edited by Pascal Fontaine.
250 $a 1st ed. 2019.
264 1 $a Cham : $b Springer International Publishing : $b Imprint: Springer, $c 2019.
300 $a XXIII, 582 p. 1901 illus., 56 illus. in color. $b online resource.
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
347 $a text file $b PDF $2 rda
490 1 $a Lecture Notes in Artificial Intelligence ; $v 11716
505 0 $a Automated Reasoning for Security Protocols -- Computer Deduction and (Formal) Proofs in Mathematics -- From Counter-Model-based Quantifier Instantiation to Quantifier Elimination in SMT -- The CADE-27 ATP System Competition - CASC-27 -- Unification modulo Lists with Reverse - Relation with Certain Word Equations -- On the Width of Regular Classes of Finite Structures -- Extending SMT solvers to Higher-Order Logic -- Superposition with Lambdas -- Restricted Combinatory Unification -- dLi: Definite Descriptions in Differential Dynamic Logic -- SPASS-SATT { A CDCL(LA) Solver -- GRUNGE: A Grand Unified ATP Challenge -- Model Completeness, Covers and Superposition -- A Tableaux Calculus for Default Intuitionistic Logic -- NIL: Learning Nonlinear Interpolants -- ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E -- Towards Physical Hybrid Systems -- SCL -- Clause Learning from Simple Models -- Names are not just Sound and Smoke: Word Embeddings for Axiom Selection -- Computing Expected Runtimes for Constant Probability Programs -- Automatic Generation of Logical Models with AGES -- Automata Terms in a Lazy WSkS Decision Procedure -- Confluence by Critical Pair Analysis Revisited -- Composing Proof Terms -- Combining ProVerif and Automated Theorem Provers for Security Protocol Verification -- Towards Bit-Width-Independent Proofs in SMT Solvers -- On Invariant Synthesis for Parametric Systems -- The Aspect Calculus -- Uniform Substitution At One Fell Swoop -- A Formally Verified Abstract Account of Gödel's Incompleteness Theorems -- Old or Heavy? Decaying Gracefully with Age/Weight Shapes -- Induction in Saturation-Based Proof Search -- Faster, Higher, Stronger: E 2.3 -- Certified Equational Reasoning via Ordered Completion -- JGXYZ - An ATP System for Gap and Glut Logics -- GKC: a Reasoning System for Large Knowledge Bases -- Optimization Modulo the Theory of Floating-Point Numbers -- FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions. .
520 $a This book constitutes the proceeding of the 27th International Conference on Automated Deduction, CADE 27, held in Natal, Brazil, in August 2019. The 27 full papers and 7 system descriptions presented were carefully reviewed and selected from 65 submissions. CADE is the major forum for the presentation of research in all aspects of automated deduction, including foundations, applications, implementations, and practical experience. .
650 0 $a Artificial intelligence. $3 559380
650 0 $a Software engineering. $3 562952
650 0 $a Computer system failures. $3 782237
650 0 $a Mathematical logic. $2 bicssc $3 810627
650 0 $a Computer logic. $3 786340
650 1 4 $a Artificial Intelligence. $3 646849
650 2 4 $a Software Engineering. $3 669632
650 2 4 $a System Performance and Evaluation. $3 669346
650 2 4 $a Mathematical Logic and Formal Languages. $3 670059
650 2 4 $a Logics and Meanings of Programs. $3 670058
700 1 $a Fontaine, Pascal. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1078523
710 2 $a SpringerLink (Online service) $3 593884
773 0 $t Springer Nature eBook
776 0 8 $i Printed edition: $z 9783030294359
776 0 8 $i Printed edition: $z 9783030294373
830 0 $a Lecture Notes in Artificial Intelligence ; $v 9285 $3 1253845
856 4 0 $u https://doi.org/10.1007/978-3-030-29436-6
912 $a ZDB-2-SCS
912 $a ZDB-2-SXCS
912 $a ZDB-2-LNC
950 $a Computer Science (SpringerNature-11645)
950 $a Computer Science (R0) (SpringerNature-43710)