<Emphasis Type="Italic">LFTOP</Emphasis>: An <Emphasis Type="Italic">LF</Emphasis>-Based Approach to Domain-Specific Reasoning

A new approach to domain-specific reasoning is presented that is based on a type-theoretic logical framework(LF) but does not require the user to be an expert in type theory. The concepts of the domain and its related reasoning systems are formalized in LF, but the user works with the system through a syntax and interface appropriate to his/her work. A middle layer provides translation between the user syntax and LF, and allows additional support for reasoning(e.g., model checking). Thus, the complexity of the logical framework is hidden but the benefits of using type theory and its related tools are retained, such as precision and machine-checkable proofs. This approach is investigated through a number of case studies: here, the authors consider the verification of properties of concurrency. The authors have formalized a specification language (CCS) and logic (μ-calculus) in LF, together with useful lemmas, and a user-oriented syntax has been designed. The authors demonstrate the approach with simple examples. However, applying lemmas to objects introduced by the user may result in framework-level objects which cannot be translated back to the user level. The authors discuss this problem, define a notion of adequacy, and prove that in this case study, translation can always be reversed.     

A semantically complete extension sequence of the system (?)

In this paper, the method of well-combined semantics and syntax proposed by Pavelka is applied to the research of the prepositional calculus formal system (?)*. The partial constant values are taken as formulas, formulas are fuzzified in two manners of semantics and syntax, and inferring processes are fuzzified. A sequence of new extensions {(?)_n~*} of the system ? is proposed, and the completeness of (?)_n~* is proved.     

Evaluation for Small Visual Difference Between Conforming Meshes on Strain Field

This paper gives a method of quantifying small visual differences between 3D mesh models with conforming topology, based on the theory of strain fields. Strain field is a geometric quantity in elasticity which is used to describe the deformation of elastomer. In this paper we consider the 3D models as objects with elasticity. The further demonstrations are provided: the first is intended to give the reader a visual impression of how our measure works in practice; and the second is to give readers a visua...     

Adapting Backward Error Recovery to Parallel Real Time Systems

The problem of adapting backward error recovery to parallel real time systems is discussed in this paper.Because of error propagation among different cooperationg processs,an error occurring in one process may influence some important oututs in other processes.Therefore.a local output has to be delayed until its validity is confirmed globally,Shince backward error recovery adopts redundancy of computing time instead of processing equipment,the variation of the actual execution time of a cooperaing process may be very large if it works in an unreliable environment.These problems are the cooperating process may be very large if it works in an unreliable environment.These problems are the primary obstacles to be removed.Previous studies focus their attentions on how to eliminate domino-effect dynamically,But backward error recovery cannot be applied irectly in parallel real time systems even under the condition that to domino-effect exists.How to reduce output delays efficiently if nodomino-effect remains?How to estimate this delay time?How to calculate the actual execution time of every process and how to schedule these processes under an unstable condition?These problems were omitted in literature unfortunately.The interest of this paper is to provide satisfactory solutions to these problems to make it possible to adopt backward error recovery efficiently in parallel real time systems.     

A semantically complete extension sequence of the system $$\mathcal{L}^* $$

In this paper, the method of well-combined semantics and syntax proposed by Pavelka is applied to the research of the propositional calculus formal system . The partial constant values are taken as formulas, formulas are fuzzified in two manners of semantics and syntax, and inferring processes are fuzzified. A sequence of new extensions { } of the system is proposed, and the completeness of is proved.     

The multiple-parameter fractional Fourier transform

The fractional Fourier transform （FRFT） has multiplicity, which is intrinsic in fractional operator. A new source for the multiplicity of the weight-type fractional Fourier transform （WFRFT） is proposed, which can generalize the weight coefficients of WFRFT to contain two vector parameters m,n ∈ Z^M . Therefore a generalized fractional Fourier transform can be defined, which is denoted by the multiple-parameter fractional Fourier transform （MPFRFT）. It enlarges the multiplicity of the FRFT, which not only includes the conventional FRFT and general multi-fractional Fourier transform as special cases, but also introduces new fractional Fourier transforms. It provides a unified framework for the FRFT, and the method is also available for fractionalizing other linear operators. In addition, numerical simulations of the MPFRFT on the Hermite-Gaussian and rectangular functions have been performed as a simple application of MPFRFT to signal processing.     

Function S-rough sets and security-authentication of hiding law

Function S-rbugh sets are defined by R-function equivalence class, which have dynamic characteristic. Function S-rough sets have dynamic characteristic, law characteristic and law-hiding characteristic. Function S-rough sets can generate f-hiding law and f-hiding law. By engrafting, crossing, and penetrating between the information security theory and function S-rough sets, the security hiding and the authentication of f-hiding law and f-hiding law are given respectively in this paper. The fusion and share between function S-rough sets and information security theory is a new research direction of the application of information law in information system.     

Construction and enumeration of Boolean functions with maximum algebraic immunity

Algebraic immunity is a new cryptographic criterion proposed against algebraic attacks. In order to resist algebraic attacks, Boolean functions used in many stream ciphers should possess high algebraic immunity. This paper presents two main results to find balanced Boolean functions with maximum algebraic immunity. Through swapping the values of two bits, and then generalizing the result to swap some pairs of bits of the symmetric Boolean function constructed by Dalai, a new class of Boolean functions with maximum algebraic immunity are constructed. Enumeration of such functions is also given. For a given function p(x) with deg(p(x)) < , we give a method to construct functions in the form p(x)+q(x) which achieve the maximum algebraic immunity, where every term with nonzero coefficient in the ANF of q(x) has degree no less than . Supported by the National Natural Science Foundation of China (Grant No. 60673068), and the Natural Science Foundation of Shandong Province (Grant Nos. Y2007G16, Y2008G01)     

Lower estimation of approximation rate for neural networks

Let SFd and Πψ,n,d = { nj=1bjψ(ωj·x+θj) :bj,θj∈R,ωj∈Rd} be the set of periodic and Lebesgue’s square-integrable functions and the set of feedforward neural network (FNN) functions, respectively. Denote by dist (SF d, Πψ,n,d) the deviation of the set SF d from the set Πψ,n,d. A main purpose of this paper is to estimate the deviation. In particular, based on the Fourier transforms and the theory of approximation, a lower estimation for dist (SFd, Πψ,n,d) is proved. That is, dist(SF d, Πψ,n,d) (nlogC2n)1/2 . T...     

Sufficient conditions for robustness of $$\mathcal{K}\mathcal{L}$$ -stability for difference inclusions

Difference inclusions arise naturally in the study of discrete-time or sampled-data systems. We develop two novel sufficient conditions for robustness of a stability property referred to as -stability with respect to an arbitrary measure; i.e., where a continuous positive definite function of the solutions satisfies a class- estimate of time and the continuous positive definite function of the initial condition. Christopher M. Kellett was supported by the Australian Research Council under Discovery Project Grant DP0771131. Andrew R. Teel was supported by NSF grants ECS-0324679, ECS-0622253, and AFOSR grants F49620-03-1-0203 and FA9550-06-1-0134.     

The inf-sup condition for low order elements on anisotropic meshes

On a large class of two-dimensional anisotropic meshes, the infsup condition (stability) is proved for the triangular and quadrilateral finite element pairs suggested by Bernardi/Raugel and Fortin. As a consequence the pairs , and turn out to be stable independent of the aspect ratio of the elements. Both the visit of the first author in Valenciennes and the visit of the second author in Chemnitz were financed by the DFG (German Research Foundation), Sonderforschungsbereich 393.     

On Enumerating Minimal Dicuts and Strongly Connected Subgraphs

We consider the problems of enumerating all minimal strongly connected subgraphs and all minimal dicuts of a given strongly connected directed graph G=(V,E). We show that the first of these problems can be solved in incremental polynomial time, while the second problem is NP-hard: given a collection of minimal dicuts for G, it is NP-hard to tell whether it can be extended. The latter result implies, in particular, that for a given set of points , it is NP-hard to generate all maximal subsets of contained in a closed half-space through the origin. We also discuss the enumeration of all minimal subsets of whose convex hull contains the origin as an interior point, and show that this problem includes as a special case the well-known hypergraph transversal problem. This research was supported by the National Science Foundation (Grant IIS-0118635). The third and fourth authors are also grateful for the partial support by DIMACS, the National Science Foundation’s Center for Discrete Mathematics and Theoretical Computer Science. Our friend and co-author, Leonid Khachiyan tragically passed away on April 29, 2005.     

Finding tree patterns consistent with positive and negative examples using queries

This paper is concerned with the problem of finding a hypothesis in consistent with given positive and negative examples. The hypothesis class consists of all sets of at most two tree patterns and represents the class of unions of at most two tree pattern languages. Especially, we consider the problem from the point of view of the consistency problem for . The consistency problem is a problem for deciding whether there exists a consistent hypothesis with given positive and negative examples within some fixed hypothesis space. Efficient solvability of that problem is closely related to the possibility of efficient machine learning or machine discovery. Unfortunately, however, the consistency problem is known to be NP-complete for many hypothesis spaces. In this paper, the problem for the class is also shown to be NP-complete. In order to overcome this computational hardness, we try to use additional information obtained by making queries. First, we give an algorithm that, using restricted subset queries, solves the consistency problem for in time polynomial in the total size of given positive and negative examples. Next, we show that each subset query made by the algorithm can be replaced by several membership queries under some condition on a set of function symbols. As a result, we have that the consistency problem for is solved in polynomial time using membership queries. This revised version was published online in June 2006 with corrections to the Cover Date.     

Staircase visibility and computation of kernels

Let be some set of orientations, that is, . We consider the consequences of defining visibility based on curves that are monotone with respect to the orientations in . We call such curves -staircases. Two points p andq in a polygonP are said to -see each other if an -staircase fromp toq exists that is completely contained inP. The -kernel of a polygonP is then the set of all points which -see all other points. The -kernel of a simple polygon can be obtained as the intersection of all {}-kernels, with . With the help of this observation we are able to develop an algorithm to compute the -kernel of a simple polygon, for finite . We also show how to compute theexternal -kernel of a polygon in optimal time . The two algorithms are combined to compute the ( -kernel of a polygon with holes in time .This work was supported by the Deutsche Forschungsgemeinschaft under Grant No. Ot 64/5-4 and the Natural Sciences and Engineering Research Council of Canada and Information Technology Research Centre of Ontario.