Automated Reasoning About Metric and Topology
Automated Reasoning About Metric and Topology
复制标题
关于度量和拓扑的自动推理
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
M. Zakharyaschev
中科院分区：
文献类型：
--
作者：
U. Hustadt;D. Tishkovsky;F. Wolter;M. Zakharyaschev
In this paper we compare two approaches to automated reasoning about metric and topology in the framework of the logic $mathcal{MT}$ introduced in [10]. $mathcal{MT}$-formulas are built from set variablesp1,p2,... (for arbitrary subsets of a metric space) using the Booleans ∧, ∨, →, and ¬, the distance operators∃ 0}$, and the topological interior and closure operatorsI and C. Intended models for this logic are of the form $mathfrak I=(Delta,d,p_{1}^{mathfrak I},p_{2}^{mathfrak I},dots)$ where (Δ,d) is a metric space and $p_{i}^{mathfrak I} subseteq Delta$. The extension$varphi^{mathfrak I} subseteq Delta$ of an $mathcal{MT}$-formula ϕ in $mathfrak I$ is defined inductively in the usual way, with I and C being interpreted as the interior and closure operators induced by the metric, and $(exists^{<a}varphi)^{mathfrak I} = { x in Delta mid exists yin varphi^{mathfrak I} d(x,y)<a }$. In other words, $(mathbf{I}varphi)^{mathfrak I}$ is the interior of $varphi^{mathfrak I}$, $(exists^{<a}varphi)^{mathfrak I}$ is the open a-neighbourhood of $varphi^{mathfrak I}$, and $(exists^{le a}varphi)^{mathfrak I}$ is the closed one. A formula ϕ is satisfiable if there is a model ${mathfrak I}$ such that $varphi^{mathfrak I}
e emptyset$; ϕ is valid if ¬ϕ is not satisfiable.
In this paper we compare two approaches to automated reasoning about metric and topology in the framework of the logic $mathcal{MT}$ introduced in [10]. $mathcal{MT}$-formulas are built from set variablesp1,p2,... (for arbitrary subsets of a metric space) using the Booleans ∧, ∨, →, and ¬, the distance operators∃ 0}$, and the topological interior and closure operatorsI and C. Intended models for this logic are of the form $mathfrak I=(Delta,d,p_{1}^{mathfrak I},p_{2}^{mathfrak I},dots)$ where (Δ,d) is a metric space and $p_{i}^{mathfrak I} subseteq Delta$. The extension$varphi^{mathfrak I} subseteq Delta$ of an $mathcal{MT}$-formula ϕ in $mathfrak I$ is defined inductively in the usual way, with I and C being interpreted as the interior and closure operators induced by the metric, and $(exists^{<a}varphi)^{mathfrak I} = { x in Delta mid exists yin varphi^{mathfrak I} d(x,y)<a }$. In other words, $(mathbf{I}varphi)^{mathfrak I}$ is the interior of $varphi^{mathfrak I}$, $(exists^{<a}varphi)^{mathfrak I}$ is the open a-neighbourhood of $varphi^{mathfrak I}$, and $(exists^{le a}varphi)^{mathfrak I}$ is the closed one. A formula ϕ is satisfiable if there is a model ${mathfrak I}$ such that $varphi^{mathfrak I}
e emptyset$; ϕ is valid if ¬ϕ is not satisfiable.