Titlebook: Mathematical Software – ICMS 2016; 5th International Co Gert-Martin Greuel,Thorsten Koch,Andrew Sommese Conference proceedings 2016 Springe

retort

书目名称Mathematical Software – ICMS 2016影响因子(影响力)




书目名称Mathematical Software – ICMS 2016影响因子(影响力)学科排名




书目名称Mathematical Software – ICMS 2016网络公开度




书目名称Mathematical Software – ICMS 2016网络公开度学科排名




书目名称Mathematical Software – ICMS 2016被引频次




书目名称Mathematical Software – ICMS 2016被引频次学科排名




书目名称Mathematical Software – ICMS 2016年度引用




书目名称Mathematical Software – ICMS 2016年度引用学科排名




书目名称Mathematical Software – ICMS 2016读者反馈




书目名称Mathematical Software – ICMS 2016读者反馈学科排名

pancreas

Exercising Nuprl’s Open-Endednessations on closed terms. Nuprl is both computationally and type-theoretically open-ended in the sense that both its computation system and its type theory can be extended as needed by checking a handful of conditions. For example, Doug Howe characterized the computations that can be added to Nuprl in

拥挤前

Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover be used for proof irrelevant reasoning as well as for proof relevant formalizations of mathematics. In my talk, I will present my experiences doing a formalization project in Lean. One of the interesting aspects of homotopy type theory is the ability to perform synthetic homotopy theory on higher t

generic

Towards the Automatic Discovery of Theorems in GeoGebraess, the main goal in such works focused on theorem proving, cf. Java Geometry Expert or GeoGebra. A related issue, automatic discovery, remains almost unexplored in the field of dynamic geometry software..This extended abstract sketches our initial results towards the incorporation into GeoGebra, a

Middle-Ear

Efficient Knot Discrimination via Quandle Coloring with SAT and #-SATts of algebraic structures, called quandles, to arcs of knot diagrams such that certain algebraic relations hold at each crossing. The existence of a coloring (called colorability) and the number of colorings of a knot by a quandle are knot invariants that can be used to distinguish knots. We realis

纪念

Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0e proof development, a higher-order rewriting mechanism, and a tool for automatically analyzing the logical structure of Theorema-theories. Each of these three tools already proved extremely useful in the extensive formal exploration of a non-trivial mathematical theory, namely the theory of Gröbner

替代品

Automated Deduction in Ring Theoryvarious possibilities of using Prover9 in ring theory and semiring theory, in particular, associative rings, rings with involutions, semirings with cancellation laws and near-rings. We code the corresponding axioms in Prover9, check some well-known theorems, for example, Jacobson’s commutativity the

费解

Agent-Based HOL Reasoningf cooperating external specialist systems with a novel agent-based proof procedure. Key goals of the system’s development involve parallelism on various levels of the proof search, adaptability for different external specialists, and native support for reasoning in expressive non-classical logics.

笨拙的你

IRATE

Bad Primes in Computational Algebraic Geometrymodulo a number of primes and then lift the modular results to the rationals. This method is guaranteed to work if we use a sufficiently large set of good primes. In many applications, however, there is no efficient way of excluding bad primes. In this note, we describe a technique for rational reco