Abstract Ordering is a well-established concept in mathematics and also plays an important role in many areas of computer science, wherequasi-orderings, most notablywell-founded quasi-orderingsandwell-quasi-orderings,are of particular interest. This paper deals with quasi-orderings on first-order terms and introduces a new notion of unification based on a special quasi-order, known ashomeomorphic tree embedding. Historically, the development of unification theory began with the central notion ofa most general unifierbased on thesubsumption order. A unifier $\sigma$ is most general, if it subsumes any other unifier $\tau$ , that is, if there is a substitution $\lambda$ with $\tau=_{E}\sigma\lambda$ , where E is an equational theory and $=_{E}$ denotes equality under E. Since there is in general more than one most general unifier for unification problems under equational theories E, calledE-Unification, we have the notion of a complete and minimal set of unifiers under E for a unification problem $\varGamma$ , denoted as $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ . This set is still the basic notion in unification theory today. But, unfortunately, the subsumption quasi-order is not a well-founded quasi-order, which is the reason why for certain equational theories there are solvable E-unification problems, but the set $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ does not exist. They are called type nullary in the unification hierarchy. In order to overcome this problem and also to substantially reduce the number of most general unifiers, we extended the well-knownencompassment order on termsto anencompassment order on substitutions(modulo E). Unification under the encompassment order is calledessential unificationand if $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ exists, then the complete set of essential unifiers $e\mathcal{U}\Sigma_{E}(\Gamma)$ is a subset of $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ . An interesting effect is that many E-unification problems with an infinite set of most general unifiers (under the subsumption order) reduce to a problem with only finitely manyessentialunifiers. Moreover, there are cases of an equational theory E, for which the complete set of most general unifiers does not exist, theminimal and complete set of essential unifiershowever does exist. Unfortunately again, the encompassment order is not a well-founded quasi-ordering either, that is, there are still theories with a solvable unification problem, for which a minimal and complete set of essential unifiers does not exist. This paper deals with a third approach, namely the extension of the well-knownhomeomorphic embedding of termsto ahomeomorphic embedding of substitutions (modulo E). We examine the set of most general, minimal, and complete E-unifiers under the quasi-order of homeomorphic embedment modulo an equational theory E, called $\varphi U\Sigma_{E}(\Gamma)$ , and propose an appropriate definitional framework based on the standard notions of unification theory extended by notions for thetree embedding theoremor Kruskal’s theorem as it is called. The main results are that forregulartheories the minimal and complete set $\varphi\mathcal{U}\Sigma_{E}(\Gamma)$ always exists. If we restrict the E-embedding order topure E-embedding, awell-known technique in logic programming and term rewriting where the difference between variables is ignored, the set $\varphi_{\pi}\mathcal{U}\Sigma_{E}(\Gamma)$ always exists and it is even finite for any theory E.

article Share on a counterexample to W. Bibel's and E. Eder's strong completeness result for connection graph resolution Authors: Jörg H. Siekmann Univ. des Saarlandes/DFKI, Saarbrücken, Germany Univ. des Saarlandes/DFKI, Saarbrücken, GermanyView Profile , Graham Wrightson Univ. of Newcastle, New South Wales, Germany Univ. of Newcastle, New South Wales, GermanyView Profile Authors Info & Claims Journal of the ACMVolume 48Issue 101 January 2001pp 145–147https://doi.org/10.1145/363647.363697Published:01 January 2001Publication History 3citation421DownloadsMetricsTotal Citations3Total Downloads421Last 12 Months5Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

In this paper a survey of the VSE system, a CASE-tool for formal software development, is presented. Main emphasis is put on the underlying formal method and tool support, and that in particular from the deductive support perspective. In order to demonstrate its broad range of applicability and to give an impression on how to work with the system we make use of two (commercial) applications taken from the safety and the IT-security domain.

Abstract. The capabilities of a automated theorem prover's interface are essential for the effective use of (interactive) proof systems. L Ω UI is the multi-modal interface that combines several features: a graphical display of information in a proof graph, a selective term browser with hypertext facilities, proof and proof plan presentation in natural language, and an editor for adding and maintaining the knowledge base. L Ω UI is realized in an agent-based client-server architecture and implemented in the concurrent constraint programming language Oz.

Abstract We show that the DA-uniflcation problem is undecidable. That is, given two binary function symbols ⊕ and ⊗, variables and constants, it is undecidable if two terms built from these symbols can be unified provided the following DA-axioms hold: Two terms are DA-unifiable (i.e. an equation is solvable in DA) if there exist terms to be substituted for their variables such that the resulting terms are equal in the equational theory DA. This is the smallest currently known axiomatic subset of Hilbert's tenth problem for which an undecidability result has been obtained.