167 research outputs found
Proving properties of logic programs: A Progress Report
No full textWe outline the progress we have made in connection with the Alvey Grant "Proving Properties of Logic Programs" (SERC GR/D/44270 and Alvey IKBS 137). This grant runs for three years from 1st November 1985. The grant holders are Professor Alan Bundy and Dr Don Sannella and it employs or has employed Dr Fausto Giunchiglia, Frank van Harmelen, Jane Hesketh, Dr Alan Smaill and Dr Lincoln Wallen as Research Associates. Pete Madden and Andrew Stevens are attached Ph.D. students
Investigating the role of score following in automatic musical accompaniment
No full textWhen suitable accompanists are not available to a soloist musician, an alternative possibility is to use computer-generated accompaniment. A computer accompanist should interact with the soloist and adapt to the soloist's playing as a human accompanist would, both reacting to expressive nuances of tempo and to unintentional errors such as wrong or mistimed notes. Over the past 25 years, accompaniment systems have been developed, all of which employ some form of score following: the process of following a musician's progress through the score of a piece during performance. This work considers the role of score following in automatic accompaniment. In this investigation we developed a computer accompanist that employs score following. Our computer musician uses Hidden Markov Models to model the score by metrical structure and to provide accompaniment to a soloist playing monophonic music in real time, as the soloist is playing. Working with MIDI input/output, it tracks tempo fluctuations, anticipates the soloist's next note and supports some amount of unintentional deviation from the score. Qualitative evaluation, by human testers, and quantitative evaluation, using measurable criteria taken from MIREX, reported that the system performs adequately. We then used interviews with eight human accompanists to consider how well a score following system models the accompaniment process. This evaluation raises questions about the musical interaction between soloist and accompanist that have received relatively little attention. The information we gathered from interviews suggests the importance of other aspects of accompaniment, such as the sharing of shape of the performance between musicians, rather than treating the accompanist as purely subservient. We discuss the implications of these issues for the design of automated accompanists
Automated Reasoning in Quantified Modal and Temporal Logics
No full textCentre for Intelligent Systems and their ApplicationsThis thesis is about automated reasoning in quantified modal and temporal logics, with an application to formal methods. Quantified modal and temporal logics are extensions of classical first-order logic in which the notion of truth is extended to take into account its necessity or equivalently, in the temporal setting, its persistence through time.
Due to their high complexity, these logics are less widely known and studied than their propositional counterparts. Moreover, little so far is known about their mechanisability and usefulness for formal methods.
The relevant contributions of this thesis are threefold: firstly, we devise a sound and complete set of sequent calculi for quantified modal logics; secondly, we extend the approach to the quantified temporal logic of linear, discrete time and develop a framework for doing automated reasoning via Proof Planning in it; thirdly, we show a set of experimental results obtained by applying the framework to the problem of
Feature Interactions in telecommunication systems.
These results indicate that (a) the problem can be concisely and effectively modeled in the aforementioned logic, (b) proof planning actually captures common structures in the related proofs, and (c) the approach is viable also from the point of view of efficiency
Recursive Program Optimization Through Inductive Synthesis Proof Transformation
No full textThe research described in this paper involved developing transformation techniques which increase the efficiency of the noriginal program, the source, by transforming its synthesis proof into one, the target, which yields a computationally more efficient algorithm. We describe a working proof transformation sys- tem which, by exploiting the duality between mathematical induction and recursion, employs the novel strategy of optimizing recursive programs by transforming inductive proofs. We compare and contrast this approach with the more traditional approaches to program transformation, and highlight the benefits of proof transformation with regards to search, correctness, automatability and generality
Automating the Synthesis of Decision Procedures in a Constructive Metatheory
No full textWe present an approach to the automatic construction of decision procedures, via a detailed example in propositional logic. The approach adapts the methods of proof‐planning and the heuristics for induction to a new domain, that of metatheoretic procedures. This approach starts by providing an alternative characterisation of validity; the proofs of the correctness and completeness of this characterisation, and the existence of a decision procedure, are then amenable to automation in the way we describe. In this paper we identify a set of principled extensions to the heuristics for induction needed to tackle the proof obligations arising in the new problem domain and discuss their integration within the clam‐Oyster system
Supporting dependently typed functional programming with proof automation and testing
No full textDependent types can be used to capture useful properties about programs at compile time. However, developing dependently typed programs can be difficult in current
systems. Capturing interesting program properties usually requires the user to write
proofs, where constructing the latter can be both a difficult and tedious process. Additionally, finding and fixing errors in program scripts can be challenging.
This thesis concerns ways in which functional programming with dependent types
can be made easier. In particular, we focus on providing help for developing programs
that incorporate user-defined types and user-defined functions. For the purpose of supporting dependently typed programming, we have designed a framework that provides
improved proof automation and error feedback.
Proof automation is provided with the use of heuristic based tactics that automate
common patterns of proofs that arise when programming with dependent types. In
particular, we use heuristics for generalising goals and employ the rippling heuristic
for guiding inductive and non-inductive proofs. The automation we describe includes
features for caching and reusing lemmas proven during proof search and, whenever
proof search fails, the user can assist the prover by providing high-level hints.
We concentrate on providing improved feedback for the errors that occur when
there is a mismatch between the specification of a program, described with the use of
dependent types, and the behaviour of the program. We employ a QuickCheck-like
testing tool for automatically identifying these forms of errors, where the counter examples generated are used as error messages.
To demonstrate the effectiveness of our framework for supporting dependently
typed programming, we have developed a prototype based around the Coq theorem
prover. We demonstrate that the framework as a whole makes program development
easier by conducting a series of case studies. In these case studies, which involved
verifying properties of tail recursive functions, sorting functions and a binary adder, a
significant number of the proofs required were automated
Musical Acts and Musical Agents: theory, implementation and practice
No full textCentre for Intelligent Systems and their ApplicationsMusical Agents are an emerging technology, designed to provide a range of new musical opportunities to human musicians and composers. Current systems in this area lack
certain features which are necessary for a high quality musician; in particular, they lack
the ability to structure their output in terms of a communicative dialogue, and reason
about the responses of their partners.
In order to address these issues, this thesis develops Musical Act Theory (MAT).
This is a novel theory, which models musical interactions between agents, allowing a
dialogue oriented analysis of music, and an exploration of intention and communication in the context of musical performance.
The work here can be separated into four main contributions: a specification for a
Musical Middleware system, which can be implemented computationally, and allows
distributed agents to collaborate on music in real-time; a computational model of musical interaction, which allows musical agents to analyse the playing of others as part
of a communicative process, and formalises the workings of the Musical Middleware
system; MAMA, a musical agent system which embodies this theory, and which can
function in a variety of Musical Middleware applications; a pilot experiment which
explores the use of MAMA and the utility of MAT under controlled conditions.
It is found that the Musical Middleware architecture is computationally implementable, and allows for a system which can respond to both direct musical communi-
cation and extramusical inputs, including the use of a custom-built tangible interface.
MAT is found to capture certain aspects of music which are of interest — an intuitive
notion of performative actions in music, and an existing model of musical interaction.
Finally, the fact that a number of different levels — theory, architecture and implementation — are tied together gives a coherent model which can be applied to many
computational musical situations
Reactive behaviour for autonomous virtual agents using fuzzy logic
No full textOne of the fundamental aspects of a virtual environment is the virtual agents that inhabit them. In many applications, virtual agents are required to perceive input information from their environment and make decisions appropriate to their task based on their programmed reaction to those inputs. The research presented in this thesis focuses on the reactive behaviour of the agents. We propose a new control architecture to allow agents to behave autonomously in navigation tasks in unknown environments. Our behaviour-based architecture uses fuzzy logic to solve problems of agent control and action selection and which can coordinate conflicts among different operations of reactive behaviours. A Fuzzy Associative Memory (FAM) is used as the process of encoding and mapping the input fuzzy sets to the output fuzzy set and to optimise the fuzzy rules. Our action selection algorithm is based on the fuzzy α-level method with the Hurwicz criterion. The main objective of the thesis was to implement agent navigation from point to point by a coordination of planning, sensing and control. However, we believe that the reactive architecture emerging from this research is sufficiently general that it could be applied to many applications in widely differing domains where real-time decision making under uncertainty is required. To illustrate this generality, we show how the architecture is applied to a different domain. We chose the example of a computer game since it clearly demonstrates the attributes of our architecture: real-time action selection and handling uncertainty. Experimental results are presented for both implementations which show how the fuzzy method is applied, its generality and that it is robust enough to handle different uncertainties in different environments. In summary, the proposed reactive architecture is shown to solve aspects of behaviour control for autonomous virtual agents in virtual environments and can be applied to various application domains
An Algebraic Semantics of Prolog Control
No full textCentre for Intelligent Systems and their ApplicationsThe coneptual distinction between logic and
control is an important tenet of logic
programing. In practice, however, logic program languages use control strategies which profoundly affect the computational behavior of programs. For example, sequential Prolog's depth-first-left-first control is an unfair strategy under which nontermination can easily arise if programs are ill-structured. Formal analyses of logic programs therefore require an explicit formalisation of the control scheme. To this ends, this research introduces an algebraic proccess semantics of sequential logic programs written in Milner's calculus of Communicating Systems (CCS). the main contribution of this semantics is that the control component of a logic programming language is conciesly modelled. Goals and clauses of logic programs correspond semantically to sequential AND and OR agents respectively, and these agents are suitably defined to reflect the control strategy used to traverse the AND/OR computation tree for the program. The main difference between this and other process semantics which model concurrency is that the processes used here are sequential. The primary control strategy studied is standard Prolog's left-first-depth-first control. CCS is descriptively robust, however, and a variety of other sequential control schemes are modelled, including breadth-first, predicate freezing, and nondeterministic strategies. The CCS semantics for a particular control scheme is typically defined hierarchically. For example, standard Prolog control is initially defined in basic CCS using two control operators which model goal backtracking and clause sequencing. Using these basic definitions, higher-level bisimilarities are derived, ehich are more closely mappable to Prolog program constructs. By using variuos algebraic properties of the control operators, as well as the stream domain and theory of observational equivalence from CCS, a programming calculus approach to logic program analysis is permitted. Some example applications using the semantics include proving program termination, verifying transformations which use cut, and characterising some control issues of partial evaluation. Since progress algebras have already been used to model concurrency, this thesis suggests that they are an ideal means for unifying the operational semantics of the sequential and concurrent paradigms of logic programming
A Computational Model of Lakatos-style Reasoning
No full textInstitute for Computing Systems ArchitectureLakatos outlined a theory of mathematical discovery and justification,
which suggests ways in which concepts, conjectures and proofs
gradually evolve via interaction between mathematicians. Different
mathematicians may have different interpretations of a conjecture,
examples or counterexamples of it, and beliefs regarding its value or
theoremhood. Through discussion, concepts are refined and conjectures
and proofs modified. We hypothesise that: (i) it is possible to
computationally represent Lakatos's theory, and (ii) it is
useful to do so. In order to test our hypotheses we have developed a
computational model of his theory.
Our model is a multiagent dialogue system. Each agent has a copy of a
pre-existing theory formation system, which can form concepts and make
conjectures which empirically hold for the objects of interest
supplied. Distributing the objects of interest between agents means
that they form different theories, which they communicate to each
other. Agents then find counterexamples and use methods identified by
Lakatos to suggest modifications to conjectures, concept definitions
and proofs.
Our main aim is to provide a computational reading of Lakatos's
theory, by interpreting it as a series of algorithms and implementing
these algorithms as a computer program.
This is the first systematic automated realisation of Lakatos's
theory. We contribute to the computational philosophy of science by
interpreting, clarifying and extending his theory. We also contribute
by evaluating his theory, using our model to test hypotheses about it,
and evaluating our extended computational theory on the basis of
criteria proposed by several theorists. A further contribution is to
automated theory formation and automated theorem proving. The process
of refining conjectures, proofs and concept definitions requires a
flexibility which is inherently useful in fields which handle
ill-specified problems, such as theory formation. Similarly, the
ability to automatically modify an open conjecture into one which can
be proved, is a valuable contribution to automated theorem proving
- …
