國立虎尾科技大學 |

Automated Reasoning = 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings /

Record Type:	Language materials, printed : Monograph/item
Title/Author:	Automated Reasoning/ edited by Didier Galmiche, Stephan Schulz, Roberto Sebastiani.
Reminder of title:	9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings /
other author:	Galmiche, Didier.
Description:	XVIII, 724 p. 128 illus.online resource. :
Contained By:	Springer Nature eBook
Subject:	Mathematical logic. -
Online resource:	https://doi.org/10.1007/978-3-319-94205-6
ISBN:	9783319942056

Automated Reasoning = 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings /
Automated Reasoning9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings /[electronic resource] :edited by Didier Galmiche, Stephan Schulz, Roberto Sebastiani. - 1st ed. 2018. - XVIII, 724 p. 128 illus.online resource. - Lecture Notes in Artificial Intelligence ;10900. - Lecture Notes in Artificial Intelligence ;9285.

An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem -- FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics -- Superposition for Lambda-Free Higher-Order Logic -- Automated Reasoning about Key Sets -- A Tableaux Calculus for Reducing Proof Size -- FORT 2.0 -- Formalizing Bachmair and Ganzinger's Ordered Resolution Prover -- The Higher-Order Prover Leo-III -- Well-Founded Unions -- Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories -- Cubicle-W: Parameterized Model Checking on Weak Memory -- QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property -- A Why3 framework for reflection proofs and its application to GMP's algorithms -- Infinitely-valued Logic -- Uniform Substitution for Differential Game Logic -- A Logical Framework with Commutative and Non-Commutative Subexponentials -- Exploring Approximations for Floating-Point Arithmetic using UppSAT -- Complexity of Combinations of Qualitative Constraint Satisfaction Problems -- A Generic Framework for Implicate Generation Modulo Theories -- A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems -- A New Probabilistic Algorithm for Approximate Model Counting -- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems -- Cops and CoCoWeb: Infrastructure for Conuence Tools -- Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing -- Superposition with Datatypes and Codatatypes -- Efficient encodings of first-order Horn formulas in equational logic -- A FOOLish Encoding of the Next State Relations of Imperative Programs -- Constructive Decision via Redundancy-free Proof-Search -- Deciding the First-Order Theory of an Algebra of Feature Trees with Updates -- A Separation Logic with Data: Small Models and Automation -- MaedMax: A Maximal Ordered Completion Tool -- From Syntactic Proofs to Combinatorial Proofs -- A Resolution-Based Calculus for Preferential Logics -- Extended Resolution Simulates DRAT -- Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle -- Efficient Interpolation for the Theory of Arrays -- ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback -- Theories as Types -- Datatypes with Shared Selectors -- Enumerating Justifications using Resolution -- A SAT-Based Approach to Learn Explainable Decision Sets -- Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions -- An abstraction-refinement framework for reasoning with large theories -- Efficient Model Construction for Horn Logic with VLog: System Description -- Focussing, MALL and the polynomial hierarchy -- Checking Array Bounds by Abstract Interpretation and Symbolic Expressions.

This book constitutes the refereed proceedings of the 9th International Joint Conference on Automated Reasoning, IJCAR 2018, held in Oxford, United Kingdom, in July 2018, as part of the Federated Logic Conference, FLoC 2018. In 2018, IJCAR unites CADE, TABLEAUX, and FroCoS, the International Symposium on Frontiers of Combining Systems, and, for the fourth time, is part of the Federated Logic Conference. The 38 revised full research papers and 8 system descriptions presented together with two invited talks were carefully reviewed and selected from 108 submissions. The papers focus on topics such as logics, deductive systems, proof-search methods, theorem proving, model checking, verification, formal methods, and program analysis.

ISBN: 9783319942056

Standard No.: 10.1007/978-3-319-94205-6doiSubjects--Topical Terms:

810627
Mathematical logic.

LC Class. No.: QA8.9-10.3

Dewey Class. No.: 005.131

Automated Reasoning = 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings /
LDR:05073nam a22004095i 4500 001 998055
003 DE-He213
005 20200703132248.0
007 cr nn 008mamaa
008 201225s2018 gw | s |||| 0|eng d
020 $a 9783319942056 $9 978-3-319-94205-6
024 7 $a 10.1007/978-3-319-94205-6 $2 doi
035 $a 978-3-319-94205-6
050 4 $a QA8.9-10.3
072 7 $a UYA $2 bicssc
072 7 $a MAT018000 $2 bisacsh
072 7 $a UYA $2 thema
082 0 4 $a 005.131 $2 23
245 1 0 $a Automated Reasoning $h [electronic resource] : $b 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings / $c edited by Didier Galmiche, Stephan Schulz, Roberto Sebastiani.
250 $a 1st ed. 2018.
264 1 $a Cham : $b Springer International Publishing : $b Imprint: Springer, $c 2018.
300 $a XVIII, 724 p. 128 illus. $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 10900
505 0 $a An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem -- FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics -- Superposition for Lambda-Free Higher-Order Logic -- Automated Reasoning about Key Sets -- A Tableaux Calculus for Reducing Proof Size -- FORT 2.0 -- Formalizing Bachmair and Ganzinger's Ordered Resolution Prover -- The Higher-Order Prover Leo-III -- Well-Founded Unions -- Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories -- Cubicle-W: Parameterized Model Checking on Weak Memory -- QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property -- A Why3 framework for reflection proofs and its application to GMP's algorithms -- Infinitely-valued Logic -- Uniform Substitution for Differential Game Logic -- A Logical Framework with Commutative and Non-Commutative Subexponentials -- Exploring Approximations for Floating-Point Arithmetic using UppSAT -- Complexity of Combinations of Qualitative Constraint Satisfaction Problems -- A Generic Framework for Implicate Generation Modulo Theories -- A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems -- A New Probabilistic Algorithm for Approximate Model Counting -- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems -- Cops and CoCoWeb: Infrastructure for Conuence Tools -- Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing -- Superposition with Datatypes and Codatatypes -- Efficient encodings of first-order Horn formulas in equational logic -- A FOOLish Encoding of the Next State Relations of Imperative Programs -- Constructive Decision via Redundancy-free Proof-Search -- Deciding the First-Order Theory of an Algebra of Feature Trees with Updates -- A Separation Logic with Data: Small Models and Automation -- MaedMax: A Maximal Ordered Completion Tool -- From Syntactic Proofs to Combinatorial Proofs -- A Resolution-Based Calculus for Preferential Logics -- Extended Resolution Simulates DRAT -- Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle -- Efficient Interpolation for the Theory of Arrays -- ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback -- Theories as Types -- Datatypes with Shared Selectors -- Enumerating Justifications using Resolution -- A SAT-Based Approach to Learn Explainable Decision Sets -- Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions -- An abstraction-refinement framework for reasoning with large theories -- Efficient Model Construction for Horn Logic with VLog: System Description -- Focussing, MALL and the polynomial hierarchy -- Checking Array Bounds by Abstract Interpretation and Symbolic Expressions.
520 $a This book constitutes the refereed proceedings of the 9th International Joint Conference on Automated Reasoning, IJCAR 2018, held in Oxford, United Kingdom, in July 2018, as part of the Federated Logic Conference, FLoC 2018. In 2018, IJCAR unites CADE, TABLEAUX, and FroCoS, the International Symposium on Frontiers of Combining Systems, and, for the fourth time, is part of the Federated Logic Conference. The 38 revised full research papers and 8 system descriptions presented together with two invited talks were carefully reviewed and selected from 108 submissions. The papers focus on topics such as logics, deductive systems, proof-search methods, theorem proving, model checking, verification, formal methods, and program analysis.
650 0 $a Mathematical logic. $2 bicssc $3 810627
650 0 $a Artificial intelligence. $3 559380
650 0 $a Computer logic. $3 786340
650 0 $a Algorithms. $3 527865
650 0 $a Software engineering. $3 562952
650 0 $a Programming languages (Electronic computers). $3 1127615
650 1 4 $a Mathematical Logic and Formal Languages. $3 670059
650 2 4 $a Artificial Intelligence. $3 646849
650 2 4 $a Logics and Meanings of Programs. $3 670058
650 2 4 $a Algorithm Analysis and Problem Complexity. $3 593923
650 2 4 $a Software Engineering. $3 669632
650 2 4 $a Programming Languages, Compilers, Interpreters. $3 669782
700 1 $a Galmiche, Didier. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1078502
700 1 $a Schulz, Stephan. $e editor. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1289480
700 1 $a Sebastiani, Roberto. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 793360
710 2 $a SpringerLink (Online service) $3 593884
773 0 $t Springer Nature eBook
776 0 8 $i Printed edition: $z 9783319942049
776 0 8 $i Printed edition: $z 9783319942063
830 0 $a Lecture Notes in Artificial Intelligence ; $v 9285 $3 1253845
856 4 0 $u https://doi.org/10.1007/978-3-319-94205-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)