001438332 000__ 06443cam\a2200733\a\4500
001438332 001__ 1438332
001438332 003__ OCoLC
001438332 005__ 20230309004259.0
001438332 006__ m\\\\\o\\d\\\\\\\\
001438332 007__ cr\un\nnnunnun
001438332 008__ 210722s2021\\\\sz\\\\\\ob\\\\101\0\eng\d
001438332 019__ $$a1261365561$$a1266811243
001438332 020__ $$a9783030810979$$q(electronic bk.)
001438332 020__ $$a3030810976$$q(electronic bk.)
001438332 020__ $$z3030810968
001438332 020__ $$z9783030810962
001438332 0247_ $$a10.1007/978-3-030-81097-9$$2doi
001438332 035__ $$aSP(OCoLC)1261050739
001438332 040__ $$aYDX$$beng$$epn$$cYDX$$dGW5XE$$dEBLCP$$dOCLCO$$dDCT$$dOCLCF$$dOCLCO$$dOCLCQ$$dCOM$$dOCLCO$$dOCLCQ
001438332 049__ $$aISEA
001438332 050_4 $$aQA76.9.M35$$bC53 2021eb
001438332 08204 $$a004.01/51$$223
001438332 1112_ $$aCICM (Conference)$$n(14th :$$d2021 :$$cOnline)
001438332 24510 $$aIntelligent computer mathematics :$$b14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings /$$cFairouz Kamareddine, Claudio Sacerdoti Coen (eds.).
001438332 2463_ $$aCICM 2021
001438332 260__ $$aCham :$$bSpringer,$$c2021.
001438332 300__ $$a1 online resource
001438332 336__ $$atext$$btxt$$2rdacontent
001438332 337__ $$acomputer$$bc$$2rdamedia
001438332 338__ $$aonline resource$$bcr$$2rdacarrier
001438332 347__ $$atext file
001438332 347__ $$bPDF
001438332 4901_ $$aLecture notes in artificial intelligence
001438332 4901_ $$aLecture notes in computer science ;$$v12833
001438332 4901_ $$aLNCS sublibrary, SL 7, Artificial intelligence
001438332 500__ $$a"This year's meeting was supposed to be held in Timisoara, Romania, but again due to the pandemic, it was held online."--Preface
001438332 504__ $$aIncludes bibliographical references and author index.
001438332 5050_ $$aIntro -- Preface -- Organization -- Invited Talks -- Logics at Work, and Some Challenges for Computer Mathematics -- Induction in Saturation-Based Reasoning -- Doing Number Theory in Weak Systems of Arithmetic -- Contents -- Formalizations -- A Modular First Formalisation of Combinatorial Design Theory -- 1 Introduction -- 2 Background -- 2.1 Mathematical Background -- 2.2 Isabelle and Locales -- 3 The Basic Design Formalisation -- 3.1 Pre-designs -- 3.2 Basic Design Properties -- 3.3 Basic Design Operations -- 4 The Block Design Hierarchy -- 4.1 Restricting Block Size -- 4.2 Balanced Designs
001438332 5058_ $$a4.3 T-Designs -- 4.4 Uniform Replication Number -- 4.5 BIBDs and Proofs -- 4.6 BIBD Extensions -- 5 Extending the Formalisation -- 5.1 Resolvable Designs -- 5.2 Group Divisible Designs -- 5.3 Design Isomorphisms -- 5.4 Graph Theory -- 6 The Modular Approach -- 6.1 The Formal Design Hierarchy -- 6.2 The Little Theories Approach -- 6.3 Notational Benefits -- 6.4 Reasoning on Locales -- 6.5 Limitations -- 7 Conclusion and Future Work -- References -- Beautiful Formalizations in Isabelle/Naproche -- 1 Introduction -- 2 Naproche, ForTheL, and LaTeX -- 3 Example: Cantor's Theorem
001438332 5058_ $$a4 Example: König's Theorem -- 5 Example: Euclid's Theorem -- 6 Example: Furstenberg's Topological Proof -- 7 Example: The Knaster-Tarski Theorem -- 8 Outlook -- References -- Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL -- 1 Introduction -- 2 Related Work -- 3 Implication and Falsity -- 3.1 Language -- 3.2 Wajsberg 1937 -- 3.3 Wajsberg 1939 -- 3.4 Shortest Axiom -- 4 Disjunction and Negation -- 4.1 Language -- 4.2 Rasiowa 1949 -- 4.3 Russell 1908 and Bernays 1926 -- 4.4 Whitehead and Russell 1910 -- 5 Challenges and Benefits -- 6 Conclusion -- References
001438332 5058_ $$aFormalization of RBD-Based Cause Consequence Analysis in HOL -- 1 Introduction -- 2 Preliminaries -- 2.1 RBD Formalization -- 2.2 ET Formalization -- 3 Cause-Consequence Diagram Formalization -- 3.1 Formal CCD Modeling -- 3.2 Formal CCD Analysis -- 4 Conclusion -- References -- Automatic Theorem Proving and Machine Learning -- Online Machine Learning Techniques for Coq: A Comparison -- 1 Introduction -- 1.1 Contributions -- 2 Tactic and Proof State Representation -- 3 Prediction Models -- 3.1 Locality Sensitive Hashing Forests for Online k-NN -- 3.2 Online Random Forest -- 3.3 Boosted Trees
001438332 5058_ $$a4 Experimental Evaluation -- 4.1 Split Evaluation -- 4.2 Chronological Evaluation -- 4.3 Evaluation in Tactician -- 4.4 Feature Evaluation -- 5 Related Work -- 6 Conclusion -- References -- Improving Stateful Premise Selection with Transformers -- 1 Introduction -- 2 Data -- 3 Experiments -- 4 Conclusion and Future Work -- References -- Towards Math Terms Disambiguation Using Machine Learning -- 1 Introduction -- 2 Related Works -- 2.1 The DLMF Dataset -- 2.2 Part-of-Math Tagger -- 2.3 Word Sense Disambiguation in NLP -- 2.4 Machine Learning Models -- 2.5 Math Language Processing -- 3 The Dataset
001438332 506__ $$aAccess limited to authorized users.
001438332 520__ $$aThis book constitutes the refereed proceedings of the 14th International Conference on Intelligent Computer Mathematics, CICM 2021, held in Timisoara, Romania, in July 2021*. The 12 full papers, 7 system descriptions, 1 system entry, and 3 abstracts of invited papers presented were carefully reviewed and selected from a total of 38 submissions. The papers focus on advances in formalization, automatic theorem proving and learning, search and classification, teaching and geometric reasoning, and logic and systems, among other topics. * The conference was held virtually due to the COVID-19 pandemic.
001438332 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed August 5, 2021).
001438332 650_0 $$aComputer science$$xMathematics$$vCongresses.
001438332 650_0 $$aArtificial intelligence$$xMathematics$$vCongresses.
001438332 650_6 $$aInformatique$$xMathématiques$$vCongrès.
001438332 650_6 $$aIntelligence artificielle$$xMathématiques$$vCongrès.
001438332 655_7 $$aConference papers and proceedings.$$2fast$$0(OCoLC)fst01423772
001438332 655_7 $$aConference papers and proceedings.$$2lcgft
001438332 655_7 $$aActes de congrès.$$2rvmgf
001438332 655_0 $$aElectronic books.
001438332 7001_ $$aKamareddine, Fairouz D.
001438332 7001_ $$aCoen, Claudio Sacerdoti.
001438332 830_0 $$aLecture notes in computer science.$$pLecture notes in artificial intelligence.
001438332 830_0 $$aLecture notes in computer science ;$$v12833.
001438332 830_0 $$aLNCS sublibrary.$$nSL 7,$$pArtificial intelligence.
001438332 852__ $$bebk
001438332 85640 $$3Springer Nature$$uhttps://univsouthin.idm.oclc.org/login?url=https://link.springer.com/10.1007/978-3-030-81097-9$$zOnline Access$$91397441.1
001438332 909CO $$ooai:library.usi.edu:1438332$$pGLOBAL_SET
001438332 980__ $$aBIB
001438332 980__ $$aEBOOK
001438332 982__ $$aEbook
001438332 983__ $$aOnline
001438332 994__ $$a92$$bISE