scholarly journals Hierarchical Combination of Unication Algorithms (Extended Abstract)

10.29007/vb87 ◽  
2018 ◽  
Author(s):  
Serdar Erbatur ◽  
Deepak Kapur ◽  
Andrew M Marshall ◽  
Paliath Narendran ◽  
Christophe Ringeissen
Keyword(s):  
Combination Method ◽  
Critical Question ◽  
Unification Algorithm ◽  
Unification Theory ◽  
Combination Problem ◽  
Equational Theories ◽  
Novel Approach ◽  
Unification Algorithms

A critical question in unification theory is how to obtaina unification algorithm for the combination of non-disjointequational theories when there exists unification algorithmsfor the constituent theories. The problem is known to bedifficult and can easily be seen to be undecidable in thegeneral case. Therefore, previous work has focused onidentifying specific conditions and methods in which theproblem is decidable.We continue the investigation in this paper, building onprevious combination results and our own work.We are able to develop a novel approach to the non-disjointcombination problem. The approach is based on a new set ofrestrictions and combination method such that if the restrictionsare satisfied the method produces an algorithm for the unificationproblem in the union of non-disjoint equational theories.

scholarly journals Novel approach in the evaluation of ultrasound BI-RADS 3 & 4 breast masses with a combination method of elastography & Doppler

2021 ◽  
Vol 0 (0) ◽  
pp. 0
Author(s):  
MaheshKumar Mittal ◽  
Anjuna Reghunath ◽  
Chintamani Chintamani ◽  
Rajni Prasad
Keyword(s):  
Combination Method ◽  
Breast Masses ◽  
Novel Approach

scholarly journals Bounded Higher-order Unification using Regular Terms

10.29007/zhpc ◽  
2018 ◽  
Author(s):  
Tomer Libal
Keyword(s):  
Higher Order ◽  
Correctness Proof ◽  
Unification Algorithm ◽  
Higher Order Terms ◽  
Unification Algorithms

We present an algorithm for the bounded unification of higher-order terms.The algorithm extends G. P. Huet's pre-unification algorithm with rules for the generation and folding of regular terms.The concise form of the algorithm allows the reuse of the pre-unification correctness proof. Furthermore, the regular termscan be restricted in order to decide the unifiability problem.Finally, the algorithm avoids re-computation of terms in a non-deterministic search which leads to a better performance in practice when compared to other boundedunification algorithms.

scholarly journals A Resolution Calculus for Second-order Logic with Eager Unification

10.29007/zpg2 ◽  
2018 ◽  
Author(s):  
Alexander Leitsch ◽  
Tomer Libal
Keyword(s):  
Higher Order ◽  
Second Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Unification Algorithm ◽  
Efficient Search ◽  
First Order ◽  
Unification Algorithms ◽  
Second Order Logic ◽  
Resolution Calculus

The efficiency of the first-order resolution calculus is impaired when lifting it to higher-order logic. The main reason for that is the semi-decidability and infinitary natureof higher-order unification algorithms, which requires the integration of unification within the calculus and results in a non-efficient search for refutations.We present a modification of the constrained resolution calculus (Huet'72) which uses an eager unification algorithm while retaining completeness. Thealgorithm is complete with regard to bounded unification only, which for many cases, does not pose a problem in practice.

scholarly journals A decomposition structure learning algorithm in Bayesian network based on a two-stage combination method

2022 ◽  
Author(s):  
Huiping Guo ◽  
Hongru Li
Keyword(s):  
Bayesian Network ◽  
Structure Learning ◽  
Learning Algorithm ◽  
Combination Method ◽  
Target Domain ◽  
Two Stage ◽  
Decomposition Property ◽  
Novel Approach ◽  
Decomposition Structure ◽  
Before And After

AbstractDecomposition hybrid algorithms with the recursive framework which recursively decompose the structural task into structural subtasks to reduce computational complexity are employed to learn Bayesian network (BN) structure. Merging rules are commonly adopted as the combination method in the combination step. The direction determination rule of merging rules has problems in using the idea of keeping v-structures unchanged before and after combination to determine directions of edges in the whole structure. It breaks down in one case due to appearances of wrong v-structures, and is hard to operate in practice. Therefore, we adopt a novel approach for direction determination and propose a two-stage combination method. In the first-stage combination method, we determine nodes, links of edges by merging rules and adopt the idea of permutation and combination to determine directions of contradictory edges. In the second-stage combination method, we restrict edges between nodes that do not satisfy the decomposition property and their parent nodes by determining the target domain according to the decomposition property. Simulation experiments on four networks show that the proposed algorithm can obtain BN structure with higher accuracy compared with other algorithms. Finally, the proposed algorithm is applied to the thickening process of gold hydrometallurgy to solve the practical problem.

scholarly journals REGION-BASED CLASSIFICATION OF ELECTRO-OPTICAL IMAGES WITH NEURAL NETWORKS AND FUZZY LOGIC

2014 ◽  
pp. 117-123
Author(s):  
Iryna Petrosyuk ◽  
Yuri Zaichenko
Keyword(s):  
Fuzzy Logic ◽  
Fuzzy Classification ◽  
Unification Algorithm ◽  
Sensing Systems ◽  
Optical Images ◽  
Novel Approach ◽  
The Neural Network ◽  
Neuro Fuzzy ◽  
Remote Sensing Systems

This paper reports on a novel approach to the optical information processing for the hyperspectral remote sensing systems by means of developed unification algorithm of the two mathematical tools: the fuzzy logic and the neural network. New neuro-fuzzy classification algorithm for hyperspectral remote sensed images has been proposed. It is able to replace complicated empirical formulae, which require the knowledge of dependences of many input parameters that rapidly change during of range time and difficult for crisp determination.

scholarly journals Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories

2000 ◽  
Vol Vol. 4 no. 1 ◽  
Author(s):  
Alexandre Boudet
Keyword(s):  
Higher Order ◽  
Unification Algorithm ◽  
First Order ◽  
Equational Theories ◽  
Order Case ◽  
International Audience ◽  
Syntactic Theories

International audience We present an algorithm for unification of higher-order patterns modulo simple syntactic equational theories as defined by Kirchner [14]. The algorithm by Miller [17] for pattern unification, refined by Nipkow [18] is first modified in order to behave as a first-order unification algorithm. Then the mutation rule for syntactic theories of Kirchner [13,14] is adapted to pattern E-unification. If the syntactic algorithm for a theory E terminates in the first-order case, then our algorithm will also terminate for pattern E-unification. The result is a DAG-solved form plus some equations of the form λ øverlinex.F(øverlinex) = λ øverlinex. F(øverlinex^π ) where øverlinex^π is a permutation of øverlinex When all function symbols are decomposable these latter equations can be discarded, otherwise the compatibility of such equations with the solved form remains open.

scholarly journals Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory

2018 ◽  
Vol 28 ◽  
Author(s):  
JESPER COCKX ◽  
DOMINIQUE DEVRIESE
Keyword(s):  
Pattern Matching ◽  
Homotopy Type ◽  
Type Theory ◽  
Ad Hoc ◽  
Unification Algorithm ◽  
Homotopy Type Theory ◽  
Higher Dimensional ◽  
Solving Equations ◽  
Unification Algorithms ◽  
Complete Overhaul

AbstractDependently typed languages such as Agda, Coq, and Idris use a syntactic first-order unification algorithm to check definitions by dependent pattern matching. However, standard unification algorithms implicitly rely on principles such asuniqueness of identity proofsandinjectivity of type constructors. These principles are inadmissible in many type theories, particularly in the new and promising branch known as homotopy type theory. As a result, programs and proofs in these new theories cannot make use of dependent pattern matching or other techniques relying on unification, and are as a result much harder to write, modify, and understand. This paper proposes a proof-relevant framework for reasoning formally about unification in a dependently typed setting. In this framework, unification rules compute not just a unifier but also a corresponding soundness proof in the form of anequivalencebetween two sets of equations. By rephrasing the standard unification rules in a proof-relevant manner, they are guaranteed to preserve soundness of the theory. In addition, it enables us to safely add new rules that can exploit the dependencies between the types of equations, such as rules for eta-equality of record types and higher dimensional unification rules for solving equations between equality proofs. Using our framework, we implemented a complete overhaul of the unification algorithm used by Agda. As a result, we were able to replace previousad-hocrestrictions with formally verified unification rules, fixing a substantial number of bugs in the process. In the future, we may also want to integrate new principles with pattern matching, for example, the higher inductive types introduced by homotopy type theory. Our framework also provides a solid basis for such extensions to be built on.

Polytypic unification

1998 ◽  
Vol 8 (5) ◽  
pp. 527-536 ◽  
Author(s):  
PATRIK JANSSON ◽  
JOHAN JEURING
Keyword(s):  
Programming Languages ◽  
Large Class ◽  
Pattern Matching ◽  
Type Inference ◽  
Logic Programs ◽  
Unification Algorithm ◽  
First Order ◽  
Unification Algorithms

Unification, or two-way pattern matching, is the process of solving an equation involving two first-order terms with variables. Unification is used in type inference in many programming languages and in the execution of logic programs. This means that unification algorithms have to be written over and over again for different term types. Many other functions also make sense for a large class of datatypes; examples are pretty printers, equality checks, maps etc. They can be defined by induction on the structure of user-defined datatypes. Implementations of these functions for different datatypes are closely related to the structure of the datatypes. We call such functions polytypic. This paper describes a unification algorithm parametrised on the type of the terms, and shows how to use polytypism to obtain a unification algorithm that works for all regular term types.

A Complex Event Model Combination Method Based on Multiple Tuples

2014 ◽  
Vol 644-650 ◽  
pp. 1483-1487
Author(s):  
Hui Lin Wang
Keyword(s):  
Event Study ◽  
Smart Home ◽  
Dynamic Change ◽  
Temporal Characteristic ◽  
Experimental Simulation ◽  
Combination Method ◽  
Model Combination ◽  
Combination Problem ◽  
Time Space ◽  
Event Model

The combination problem of complex event model is an important problem in complex event study. Aiming to solve the problem of no well reflecting the spatial-temporal characteristic in current comeplex even models, which are combined by atomic events based on time or space or time and space, a multi-tuple combination method of complex event model based on object, time, space, events and properties is proposed in this paper based on the analysis in existing complex event model.The basic idea of the method is to make use of intrinsic relation existing in multi tuple of event model to combine and express complex event. At a result, our supposed model not only can more comprehensively reflect the spatial-temporal characteristic of event, but also can reflect some dynamic change conditions occurred in the event. Smart home temperature and humidity detection as a case and experimental simulation are used to illustrate and prove the correctness and feasibility of the proposed complex event method based on multiple tuple.

Sign in / Sign up

Export Citation Format

Share Document