Conditional Congruence Closure over Uninterpreted and Interpreted Symbols

A framework for generating congruence closure and conditional congruence closure of ground terms over uninterpreted as well as interpreted symbols satisfying various properties is proposed. It is based on some of the key concepts from Kapur's congruence closure algorithm(RTA97)for ground equations based on introducing new symbols for all nonconstant subterms appearing in the equation set and using ground completion on uninterpreted constants and puri?ed equalities over interpreted symbols belonging to different theories. In the original signature, the resulting rewrite systems may be nonterminating but they still generate canonical forms. A byproduct of this framework is a constant Horn completion algorithm using which ground canonical Horn rewrite systems can be generated for conditional ground theories.New effcient algorithms for generating congruence closure of conditional and unconditional equations on ground terms over uninterpreted symbols are presented. The complexity of the conditional congruence closure is shown to be O(n*log(n)), which is the same as for unconditional ground equations.The proposed algorithm is motivated by our attempts to generate effcient and succinct interpolants for the quanti?er-free theory of equality over uninterpreted function symbols which are often a conjunction of conditional equations and need additional simpli?cation. A completion algorithm to generate a canonical conditional rewrite system from ground conditional equations is also presented. The framework is general and ?exible and is used later to develop congruence closure algorithms for cases when function symbols satisfy simple properties such as commutativity, nilpotency, idempotency and identity as well as their combinations. Interesting outcomes include algorithms for canonical rewrite systems for ground equational and conditional theories on uninterpreted and interpreted symbols leading to generation of canonical forms for ground terms, constrained terms and Horn equations.

NuMDG:A New Tool for Multiway Decision Graphs Construction

Multiway Decision Graphs （MDGs） are a canonical representation of a subset of many-sorted first-order logic. This subset generalizes the logic of equality with abstract types and uninterpreted function symbols. The distinction between abstract and concrete sorts mirrors the hardware distinction between data path and control. Here we consider ways to improve MDGs construction. Efficiency is achieved through the use of the Generalized-If-Then-Else （GITE） commonly operator in Binary Decision Diagram packages. Consequently, we review the main algorithms used for MDGs verification techniques. In particular, Relational Product and Pruning by Subsumption are algorithms defined uniformly through this single CITE operator which will lead to a more efficient implementation. Moreover, we provide their correctness proof. This work can be viewed as a way to accommodate the ROBBD algorithms to the realm of abstract sorts and uninterpreted functions. The new tool, called NuMDG, accepts an extended SMV language, supporting abstract data sorts. Finally, we present experimental results demonstrating the efficiency of the NuMDG tool and evaluating its performance using a set of benchmarks from the SMV package.

A Minimalist Account of Wh-Movement in Fulfulde

Operator movement is one of the scholastic views which have been advanced to analyse expressions that contain an operator of some kind.In this work,attention will be focused on interrogative operator in Fulfulde.This work examines the nature of wh-movement in Fulfulde using the minimalist programme.In conducting the research,primary and secondary sources of data collection were employed.The native speaker’s intuition forms the primary source of data while the secondary source involves three competent native speakers of Adamawa Fulfulde to validate the data.The outcome of the study reveals four types of wh-movement in Fulfulde.The four types of wh-movement in Fulfulde are the subject preposed from its canonical position in declarative sentences to a new position in interrogative sentences.There are both left to right movement and right to left movement.The interrogative questions are marked by an optional‘na’at the end of the sentence.It is possible and grammatical to have double interrogatives but only one of the elements can move.The movement is determined by proximity,short or long movement of the interrogative marker to either left to right or right to left.However,wh-or interrogative element in Fulfulde is represented by-ye and-e suffixes bound to stems of pronouns and some prepositions.Pied-piping and preposition stranding are also observed.In some whmovement,the question remains in place called wh-in-situ;here,the interrogative marker does not move at all.When this happens the interrogative marker occupies the position of the element in question.When there is movement,each move element leaves behind a trace marked by‘t’and the trace is co-indexed so that we can see the extraction sites and the landing sites of the elements that have moved.The direct object preposed to the complementizer position through wh-movement and the subject of the main clause raises and moves into the subject position of the relative clause in order to check the question feature of comp in Fulfulde.