Automated reasoning about elementary point-set topology

DOI10.1007/BF00243005MaRDI QIDQ1122363zbMATH OpenOpenAlexFDO

Authors Cynthia A. Wick, William McCune

Publication date 1989

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00243005

zbMATH Keywords

automated reasoningresolutionset theorysorted logictopology

Mathematics Subject Classification ID

Review text

The authors use a first-order formulation of point set topology using sorted logic where one has three types of objects: viz., points, sets of points and collections of sets of points. The use of typed variables, however, presents difficulties when one applies automated reasoning. The authors try to get around this difficulty by using ``implicit typing where the position of an argument determines its type. Using this formal framework the authors describe the basic notions of point set topology and they give a resolution proof of the fact that a basis generates a topology with that basis.

Recommendations

• Automated Reasoning About Metric and Topology
• scientific article; zbMATH DE number 4160159
• scientific article; zbMATH DE number 4160161
• scientific article; zbMATH DE number 2247478
• Automated reasoning in geometry
• Elementary computable topology
• A system for computing and reasoning in algebraic topology
• scientific article; zbMATH DE number 1762070
• Elementary point-set topology. A transition to advanced mathematics

Cited in

(3)

• scientific article; zbMATH DE number 4160159 (Why is no real title available?)
• Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
• Mathematical induction in Otter-lambda

Describes a project that uses

Uses Software

• AURA

This page was built for publication: Automated reasoning about elementary point-set topology

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1122363)