In this paper we show that the critical part of a correctness proof for implementations of higher-order functional languages is amenable to machine-assisted proof. An extended version of the lambda-calculus is conside...
详细信息
ISBN:
(纸本)3540600175
In this paper we show that the critical part of a correctness proof for implementations of higher-order functional languages is amenable to machine-assisted proof. An extended version of the lambda-calculus is considered, and the congruence between its direct and continuation semantics is proved. the proof has been constructed withthe help of a generic theorem prover - Isabelle. the major part of the problem lies in establishing the existence of predicates which describe the congruence. this has been solved using Milne's inclusive predicate strategy [5]. the most important intermediate results and the main theorem as derived by Isabelle are quoted in the paper.
the proceedings contain 44 papers. the special focus in this conference is on Machine Learning. the topics include: Reasoning and learning in probabilistic and possibilistic networks;problem decomposition and the lear...
ISBN:
(纸本)3540592865
the proceedings contain 44 papers. the special focus in this conference is on Machine Learning. the topics include: Reasoning and learning in probabilistic and possibilistic networks;problem decomposition and the learning of skills;machine learning in the world wide web;towards a new method for theorizing about adaptive agents;learning abstract planning cases;the role of prototypicality in exemplar-based learning;specialization of recursive predicates;a distributed genetic algorithm improving the generalization behavior of neural networks;learning non-monotonic logic programs;a comparative utility analysis of case-based reasoning and control-rule learning systems;a minimization approach to propositional inductive learning;on concept space and hypothesis space in case-based learning algorithms;the power of decision tables;pruning multivariate decision trees by hyperptane merging;multiple-knowledge representations in concept learning;the effect of numeric features on the scalability of inductive learning programs;analogical logic program synthesis from examples;a guided tour through hypothesis spaces in ilp;puzzling together RUth and SPECTRE;discovery of constraints and data dependencies in relational databases;learning disjunctive normal forms in a dual classifier system;the effects of noise on efficient incremental induction;analysis of Rachmaninoff's piano performances using inductive logicprogramming;handling real numbers in inductive logicprogramming;simplifying decision trees by pruning and grafting;a tight integration of pruning and learning;decision-tree based neural network;learning reeursion with iterative bootstrap induction;patching proofs for reuse;adapting to drift in continuous domains and parallel recombinative reinforcement learning.
the proceedings contain 26 papers. the special focus in this conference is on Higher Order logictheorem Proving and Its Applications. the topics include: Non-primitive recursive function definitions;experiments with ...
ISBN:
(纸本)3540602755
the proceedings contain 26 papers. the special focus in this conference is on Higher Order logictheorem Proving and Its Applications. the topics include: Non-primitive recursive function definitions;experiments with ZF set theory in HOL and isabelle;automatically synthesized term denotation predicates;on the refinement of symmetric memory protocols;combining decision procedures in the HOL system;deciding cryptographic protocol adequacy with HOL;a practical method for reasoning about distributed systems in a theorem prover;a theory of finite maps;virtual theories;an automata theory dedicated towards formal circuit synthesis;interfacing HOL90 with a functional database query language;floating point verification in HOL;automation and application;a formulation of TLA in isabelle;formal verification of serial pipeline multipliers;a tool for window inference in HOL;formal verification of counterflow pipeline architecture;deep embedding VHDL;higher order logic of computable functions;a mechanized logic for secure key escrow protocol verification;very efficient conversions;recording and checking HOL proofs;formalization of planar graphs;a hierarchical method for reasoning about distributed programming languages.
the paper presents AATMA: a technology mapping algorithm for antifuse based FPGAs. the algorithm is independent of the logic module structure. It can handle large libraries with complex functions and uses a signature-...
详细信息
the paper presents AATMA: a technology mapping algorithm for antifuse based FPGAs. the algorithm is independent of the logic module structure. It can handle large libraries with complex functions and uses a signature-matching based approach to achieve high mapping quality and shorter execution times. this makes it a powerful tool not only for mapping designs onto a logic module but also for the design and evaluation of antifuse-based FPGA logic module architectures. the details of the overall algorithm along withthe signature matching technique are presented. the experimental results show that AATMA needs upto 15-20% fewer logic modules than MISII and is upto 15 to 20 times faster.
the introduction of multiplexer based FPGAs has renewed interest in logic design using multiplexers. this paper presents an iterative approach for the synthesis of combinational circuits using a tree network of 2-to-1...
详细信息
the introduction of multiplexer based FPGAs has renewed interest in logic design using multiplexers. this paper presents an iterative approach for the synthesis of combinational circuits using a tree network of 2-to-1 multiplexers. A characterizing parameter of Boolean functions, known as Ratio Parameters, has been used in each iteration to reduce the search space. the obtained multiplexer network is then mapped onto the Actel ACT1 FPGA basic blocks. the performance of the proposed approach has been evaluated by comparing the results of 11 MCNC benchmark problems withthe results of the existing technology mappers.
the proceedings contain 38 papers. the special focus in this conference is on Lambda Calculus and Proof theory. the topics include: Subtyping with singleton types;a subtyping for the fisher-honsell-mitchell lambda cal...
ISBN:
(纸本)9783540600176
the proceedings contain 38 papers. the special focus in this conference is on Lambda Calculus and Proof theory. the topics include: Subtyping with singleton types;a subtyping for the fisher-honsell-mitchell lambda calculus of objects;the girard translation extended with recursion;decidability of higher-order subtyping with intersection types;formalising undefinedness in typed lambda calculus;lambda representation of operations between different term algebras;semi-unification and generalizations of a particularly simple form;a mixed linear and non-linear logic;cut free formalization of logic with finitely many variables;monadic second-order logic and linear orderings of finite structures;first-order spectra with one binary predicate;monadic logical definability of NP-complete problems;logics for context-free languages;log-approximable minimization problems on random inputs;is first order contained in an initial segment of PTIME;logicprogramming in tau categories;reasoning and rewriting with set-relatlons I;resolution games and non-liftable resolution orderings;on existential theories of list concatenation;completeness of resolution for definite answers with case analysis;subrecursion as a basis for a feasible programming language;a sound metalogical semantics for input/output effects;an intultionistlc modal logic with applications to the formal verification of hardware;towards machine-checked compiler correctness for higher-order pure functional languages;canonical forms for data-specifications;an algebraic view of structural induction;on the interpretation of type theory in locally cartesian closed categories;algorithmic aspects of propositional tense logics;stratified default theories;ramified recurrence and computational complexity II and general form recursive equations I.
the proceedings contain 27 papers. the special focus in this conference is on Object-Oriented programming. the topics include: Methods as assertions;abstracting process-to-function relations in concurrent object-orien...
ISBN:
(纸本)9783540582021
the proceedings contain 27 papers. the special focus in this conference is on Object-Oriented programming. the topics include: Methods as assertions;abstracting process-to-function relations in concurrent object-oriented applications;typed concurrent objects;atomic object composition;patterns generate architectures;meta patterns - a means for capturing the essentials of reusable object-oriented design;modeling object-oriented program execution;hypermedia as the subject matter and the medium for computer-supported cooperative work;object-oriented computations in logicprogramming;deductive object databases;declarative object-oriented programming;constraints and object identity;protection in the guide object-oriented distributed system;object location control using meta-level programming;customising object allocation;combining object-oriented analysis and formal description techniques;a specification language for object-oriented analysis and design;real-time specification inheritance anomalies and real-time filters;efficient dynamic look-up strategy for multi-methods;generalizing dispatching in a distributed object system;adding digital video to an object-oriented user interface toolkit and product configurations - an application for prototype object approach.
Because current robot teaching methods are inadequate to fully control a higli accuracy manipulator, the concept of a graphical interface which combines both teaching and programming methods is presented here. the com...
详细信息
the Hoist Scheduling Problem in electroplating facilities is known as an NP-Hard and strongly constrained problem. Up to now, the Operational Research approach appeared to be limited to the resolution of specific kind...
详细信息
ISBN:
(纸本)185166839X
the Hoist Scheduling Problem in electroplating facilities is known as an NP-Hard and strongly constrained problem. Up to now, the Operational Research approach appeared to be limited to the resolution of specific kinds of lines. We have proposed a new approach using the Constraint logicprogramming. In this paper we give a model for simple lines, aiming at providing the optimal solution for the 1-periodic problem, and that can easily be extended. then we compare the performances of two kinds of solvers: PROLOG III that uses rational variables, and CHIP that uses finite domains. We finally give results for a benchmark example.
暂无评论