Titlebook: Intelligent Computer Mathematics; 10th International C Herman Geuvers,Matthew England,Olaf Teschke Conference proceedings 2017 Springer Int

天赋

Reasoning with Concept Diagrams About Antipatterns in Ontologies,se (merged) diagrams are easier to comprehend for users than a set of lower level diagrams that are a one-to-one translation from OWL ontology axioms. We prove that our inference rules are sound, and exemplify how they can be used to reason about inconsistencies and incoherence.

CLEFT

OATH

CESS

冥想后

审问,审讯

Pessary

The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema,hand, we compare the mathematical setup of the two theories and, on the other hand, we also give an overview on statistical indicators, such as number of auxiliary lemmas and the total number of proof steps needed for all proofs in the theory. Last but not least, we present a shorter version of proo

Mast-Cell

Automatically Proving Equivalence by Type-Safe Reflection,o construct and manipulate proofs. We build a hierarchy of tactics for proving equivalences in semi-groups, monoids, commutative monoids, groups, commutative groups, semi-rings and rings. We also show how each tactic reuses those from simpler structures, thus avoiding duplication of code and proofs.

小隔间

absorbed

Classification of Alignments Between Concepts of Formal Mathematical Systems,rom different formal proof libraries or semi-formal libraries even if the latter is based on a different mathematical foundation. We present a classification of alignments and design a simple format for describing alignments, as well as an infrastructure for sharing them. We propose these as a centr