In the same way the more conventional fields of computer science need some theory, including the mathematical foundations of the calculus and the establishment of formal models, neural computation also needs its own. ...
详细信息
ISBN:
(纸本)3540630473
In the same way the more conventional fields of computer science need some theory, including the mathematical foundations of the calculus and the establishment of formal models, neural computation also needs its own. the basic requirements of this model are modularity, "small grain", high connectivity, parametric local computation and some capacity of self-programming by means of the adjustment of these parameters. We present here a proposal in this line that allows the integration in a single frame of all current models (analogic, logic and inferential) and makes clear the natural way to bridge the symbolic and connectionistic perspectives of AI extending the model of local computation to hierarchic graphs, building networks by joining graphs and studying the set of operators we need for modifying local computation parameters values.
the proceedings contain 19 papers. the special focus in this conference is on Hybrid Systems. the topics include: Bumpless switching in hybrid systems;a toolbox for proving and maintaining hybrid specifications;simula...
ISBN:
(纸本)3540633588
the proceedings contain 19 papers. the special focus in this conference is on Hybrid Systems. the topics include: Bumpless switching in hybrid systems;a toolbox for proving and maintaining hybrid specifications;simulation of hybrid systems;application of the kohn-nerode control law extraction procedure to the inverted pendulum problem;decidability of hybrid systems with linear and nonlinear differential inclusions;reliable implementation of hybrid control systems for advanced avionics;a formalism and a programming language for dynamic networks of hybrid automata;synthesis of minimally restrictive legal controllers for a class of hybrid systems;control theory, modal logic, and games;agent based velocity control of highway systems;a computational analysis of the reachability problem for a class of hybrid dynamical systems;a class of rectangular hybrid systems with computable reach set;safe implementations of supervisory commands;hybrid system games: extraction of control automata with small topologies;hybrid control desgin for a three vehicle scenario demonstration using overlapping decompositions;towards continuous abstractions of dynamical and control systems;a totally ordered set of discrete abstractions for a given hybrid or continuous system;comparing timed and hybrid automata as approximations of continuous systems and hybrid control models of next generation air traffic management.
Object-oriented constraint programming (OOCP) combines two orthogonal but complementary programming paradigms into one-object-oriented programming (OOP) and logic constraint programming (LCP). Most practitioners of OO...
详细信息
ISBN:
(纸本)081868271X
Object-oriented constraint programming (OOCP) combines two orthogonal but complementary programming paradigms into one-object-oriented programming (OOP) and logic constraint programming (LCP). Most practitioners of OOCP would agree that the design of a constraint-based model is the most time consuming and difficult part of OOCP. there is currently no systematic approach or methodology to follow when designing a model suitable for OOCP. the paper outlines a simple methodology that extends traditional object-oriented analysis and design (OOAD) to cover constrained variables and constraints used in OOCP. the proposed OOCP Methodology is an initial investigation into providing a more rigid set of guidelines to follow when designing constraint-based models. the paper presents the OOCP methodology using a simplified nurse rostering system as a case study.
the existing Z supporting tools focus on providing editing and syntax checking functionalities (Siddiqi et al., 1993). We develop VZ (Visual Z) visual programming environment for constructing Z specifications. the mai...
详细信息
the existing Z supporting tools focus on providing editing and syntax checking functionalities (Siddiqi et al., 1993). We develop VZ (Visual Z) visual programming environment for constructing Z specifications. the main advantage of such an environment is to allow the user to manipulate icons (glyphs) to generate a specification. Instead of remembering the set of Z symbols, the user can manipulate the visually understandable icons to develop the specification. Moreover, VZ is a well organized environment; various components of a specification are organized into different folders for easy storage and retrieval. Finally, VZ also supports validation of specification and basic logic proving, which are essential in developing correct specification.
the proceedings contain 20 papers. the special focus in this conference is on algebraic and logicprogramming. the topics include: Concurrent constraint programming;specifications using multiple-conclusion logic progr...
ISBN:
(纸本)9783540584315
the proceedings contain 20 papers. the special focus in this conference is on algebraic and logicprogramming. the topics include: Concurrent constraint programming;specifications using multiple-conclusion logic programs;viewing a program transformation system at work;proving implications by algebraic approximation;sufficient completeness and parameterized proofs by induction;proving behavioural theorems with standard first-order logic;compositional analysis for equational horn programs;equation solving in projective planes and planar ternary rings;concurrent logicprogramming as uniform linear proofs;three-valued completion for abductive logic programs;a sequential reduction strategy;on modularity of termination and confluence properties of conditional rewrite systems;syntactical analysis of total termination;logic programs as term rewriting systems;higher-order minimal function graphs;reasoning about layered, wildcard and product patterns;preserving universal termination through unfold/fold and a logic for variable aliasing in logic programs.
Discusses the current situation of formal methods and their use in the re-engineering of computing systems, especially real-time systems. Based on the analysis results, a solution which uses a consistent 4-sector Wide...
详细信息
Discusses the current situation of formal methods and their use in the re-engineering of computing systems, especially real-time systems. Based on the analysis results, a solution which uses a consistent 4-sector Wide Spectrum Language (WSL) is proposed, which presently includes the general architecture and work flow, the structure of the Object-Action Model, the syntax and semantics of the Object-oriented Temporal Agent Model (ObTAM) and the Timed Guarded Command Language (TGCL). A small case study shows an optimistic future for our WSL technique. Further research will aim to build the complete semantic kernel of the WSL and its associated algebraic laws, including transformation rules and abstraction rules.
In this paper, we propose a three-valued completion semantics for abductive logic programs, which solves some problems associated withthe Console et al. two-valued completion semantics. the semantics is a generalizat...
详细信息
In this paper, we propose a three-valued completion semantics for abductive logic programs, which solves some problems associated withthe Console et al. two-valued completion semantics. the semantics is a generalization of Kunen's completion semantics for general logic programs, which is known to correspond very well to a class of effective proof procedures for general logic programs. Secondly, we propose a proof procedure for abductive logic programs, which is a generalization of a proof procedure for general logic programs based on constructive negation. this proof procedure is sound and complete with respect to the proposed semantics. By generalizing a number of results on general logic programs to the class of abductive logic programs, we present further evidence for the idea that limited forms of abduction can be added quite naturally to general logic programs.
the theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logicprogramming languages. Two such languages, lambda Prolog and its linear logic refinement, Lolli [15], provide...
详细信息
the theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logicprogramming languages. Two such languages, lambda Prolog and its linear logic refinement, Lolli [15], provide for various forms of abstraction (modules, abstract data types, and higher-order programming) but lack primitives for concurrency. the logicprogramming language, LO (Linear Objects) [2] provides some primitives for concurrency but lacks abstraction mechanisms. In this paper we present Forum, a logicprogramming presentation of all of linear logicthat modularly extends lambda Prolog, Lolli, and LO. Forum, therefore, allows specifications to incorporate both abstractions and concurrency. To illustrate the new expressive strengths of Forum, we specify in it a sequent calculus proof system and the operational semantics of a programming language that incorporates references and concurrency. We also show that the meta theory of linear logic can be used to prove properties of the object-languages specified in Forum.
We introduce a compositional characterization of the operational semantics of equational Horn programs. then we show that this semantics and the standard operational semantics based on (basic) narrowing coincide. We d...
详细信息
We introduce a compositional characterization of the operational semantics of equational Horn programs. then we show that this semantics and the standard operational semantics based on (basic) narrowing coincide. We define an abstract narrower mimicking this semantics, and show how it can be used as a basis for efficient AND-compositional program analysis. As an application of our framework, we show a compositional analysis to detect the unsatisfiability of an equation set with respect to a given equational theory. We also show that our method allows us to perform computations and analysis incrementally in a Constraint Equational setting and that the test of satisfiability in this setting can be done in parallel.
暂无评论