Systems which combine various forms of reasoning such as deductive inference and symbolic manipulation have repeatedly been shown to be more effective than stand-alone systems. In general, however, the combined systems are ad-hoc and designed for a single task. We present a generic framework for combining reasoning processes which is based on the theory of the Global Workspace Architecture. Within this blackboard-style framework, processes attached to a workspace propose information to be broadcast, along with a rating of the importance of the information, and only the most important is broadcast to all the processes, which react accordingly. To begin to demonstrate the value of the framework, we show that the tasks undertaken by previous ad-hoc systems can be performed by a configuration of the framework. To this end, we describe configurations for theorem discovery and conjecture making respectively, which produce comparable results to the previous ICARUS and HOMER systems. We further describe a novel application where we use a configuration of the framework to identify potentially interesting specialisations of finite algebras.
The framework then broadcasts only the highest rated proposal at the start of the next round, and the session progresses. Developers of combined reasoning systems can configure the framework to perform particular tasks by specifying how certain processes will reason about certain types of information; what novel information they will output; and how proposals should be ranked.
Automated theory formation, as performed by the HR system [
As described in x3 and x4 respectively, we have managed to configure the framework to perform automated theorem discovery in quasigroup theory (as previously undertaken by HR as part of the ICARUS system) and to perform automated conjecture making in number theory (as previously undertaken by the HOMER system). For each configuration, we describe the processes, the types of information which are broadcast, and how this information is rated. We also provide qualitative and quantitative comparisons with ICARUS and HOMER respectively. In x5, we describe a new application for combined reasoning systems in the domain of finite algebra. In this application, we seek to identify specialisations of finite algebras which are simple in definition yet have mathematical properties to suggest they may be interesting areas for mathematical investigation in their own right. The configuration we developed for this task is a modified version of the one we used in x3 for automated theorem discovery in quasigroup theory. We applied this to three different classes of finite algebra and, in each case, the system identified an interesting specialisation.
A Global Workspace Architecture is essentially a model of combined serial and parallel information
flow, wherein specialist sub-processes compete and co-operate for access to a global workspace [
The architecture defined by our framework is inspired by the Global Workspace Architecture [
At the end of each round, various processes will have been added to and removed from the global workspace, and a set of broadcast proposals will have been submitted to the framework. At the start of the next round, the framework chooses the proposal with the highest importance value, and broadcasts the reasoning artefact from that proposal. In the case where multiple proposals have equal heuristic value, one is chosen from them randomly. All non-broadcast proposals are discarded and will not be considered for broadcast later unless they are re-proposed. Currently, all reasoning artefacts are broadcast as string arrays, examples of which are presented in the next two sections.
To create a combined system, a developer must create a configuration of the framework, by defining:
The processes that may be attached to the workspace and their behaviour, which must conform to the framework rules. In particular, how each process reacts to broadcasts, the processing or reasoning they perform, the proposals they can make and the method they use in determining the heuristic rating of importance.
We have developed the GC toolkit, which enables developers to easily configure combinations of
reasoning systems for particular tasks within the framework. GC, which takes its name from global-workspace
and combining, allows users to develop their configurations into full system implementations. It includes
the core code for the round-by-round processing and a number of pre-coded processes which
encapsulate specific reasoning tasks. For example, the toolkit currently provides a process which appeals to the
Prover9 theorem prover [
The GC toolkit is implemented in Java. Developers who wish to create new processes do so by extending the toolkit’s WorkspaceProcess class. This class defines an abstract method react which the developer must override with the behaviour they want for their process. The react method must implement how the process behaves in response to different broadcasts and the processing that should be performed. The react method should return whatever proposals the developer wishes the process to make, and the developer must also define how the process should rate the importance of its proposals. The developer can also define parameters for the process. For example, a process to read and broadcast the contents of a file benefits from a parameter to indicate the file path. If a developer wishes to encapsulate an external reasoning system then the react method should be a wrapper for that system, making appropriate external calls. The toolkit includes a graphical interface for creating configurations of the framework. It allows users to drag and drop processes into configurations, set their parameters and run the resulting configurations. The code that runs the workspace simply calls the react method for all currently attached processes, collates their returned proposals and selects the highest rated.
Our framework is quite straightforward and we have only deviated from the underlying GWA theory by allowing the termination and spawning of processes. We believe that maintaining this low complexity has several benefits for clarity of design and extensibility, and we are investigating how capable this simple framework can be. However, there are many areas of the framework where we see potential for future development. For example, currently, all processing is performed on a single processor in a serial fashion. Moreover, processing is synchronous, because all processes are given the chance to react before a new round is begun, and it may be that parallel or asynchronous variants of the framework could be more effective. Further, once started, the behaviour of the system will be determined by three factors: the configuration chosen by the user, the values of parameters they have set and the randomness in choosing between equal proposals in a given round. Currently, once processing has begun, the user cannot intervene in any way other than to pause or stop the system. We have introduced control processes and control broadcasts, in response to which some processes detach from the workspace. This allows us to terminate some aspects of processing when a specific processing goal has been reached. However, we have not yet considered any more sophisticated intervention schemes. As yet, we have only considered relatively simple importance rating schemes. In general, processes will assign the same importance to all broadcasts of the same type. We have enhanced this slightly in some applications where we enable processes to determine the importance of their proposals based upon the specifics of their proposal. For example, in x3.4, the importance rating is based partly upon the number of predicates and variables included in a concept defintion. These, and other, aspects of the framework, where we see the potential for future development are discussed in x6.
In the next sections, we present configurations of the framework to demonstrate its potential for
combining reasoning systems. In the first configuration, we develop the core automated theory formation
processes which achieves similar behaviour to the concept production rules, conjecture making routines
and third-party interactions which drive the HR system. These processes appeal to both the Yap Prolog
system [
Constraint solving is a very successful area of Artificial Intelligence research, and constraint solvers
are regularly used for solving industrial-strength problems in, for example, scheduling or bin-packing.
The way in which a constraint satisfaction problem (CSP) is specified is crucial to the success of the
solver, as different specifications can lead to radically quicker solving times. For this reason, there
has been much research into reformulating constraint satisfaction problems. Our contribution has been
to introduce a combined-reasoning system for finding additional constraints which are implied by the
CSP specification. With the ICARUS system [
With the configuration described here, we intended to show that the framework could combine machine learning and theorem proving processes to discover implied constraints about QG-quasigroups similar to those found by ICARUS. In future, we also plan to attach constraint solving processes, so that the framework will be able to determine – like ICARUS – which implied constraints reduce solving time. As described in x3.1 to x3.4 below, to configure the framework for this task, we specified five different types of broadcastable artefacts, some concept forming, conjecture making and explanation finding processes and a fairly straightforward scheme for ascribing importance values to bids for artefacts to be broadcast. In x3.5, we show that the configured framework does indeed produce similar results to ICARUS.
In overview, the configured framework was required to invent new concepts (initially built from a set of user-supplied background concepts), by manipulating and combining existing concept definitions. Concept defintions are first order logic statements in a Prolog-readable format. Each concept definition partitions the example set into two; those for which the definition holds and those for which it does not. By comparing the sets of examples for which definitions hold, the system makes empirical conjectures which relate the concepts. Some of these conjectures can be proven to follow from the axioms of the domain of investigation. In simple outline, the system starts with Definition broadcasts for the background concept definitions. The DefinitionReviewer acts as a filter, so that only unique Definitions become Concepts. The ExampleFinder process finds examples for Concepts and the EquivalenceReviewer process filters out those Concepts that are equivalent to previous Concepts. When a Concept has passed this filter, a NewConcept is broadcast. DefinitionCreator processes react to NewConcept broadcasts by manipulating their definitions to create new Definitions. NewConcept broadcasts also feed into conjecture making. In particular, ImplicationMaker processes compare the example sets of NewConcepts and propose Conjectures, which may be proved by the Prover process, creating an Explanation proposal. Full details of broadcastable artefacts and the processes are given below. 3.1
To represent the concepts, conjectures and proofs, we specified five main types of broadcast artefacts, below. As noted in x2, broadcasts take the form of string arrays, and we use the notation [e0 : e1 : : : : : en] to represent such an array of strings. In general, the first element of a broadcast string array indicates the type of broadcast. The remaining elements are the specifics of that broadcast. 1. Definition, in the form [def:D], where D is a Prolog-readable definition of a concept. 2. Concept, in the form [conc:D:E], with D as above and E being a list of examples which satisfy that concept definition. 3. NewConcept, in the form [new:D:E], with D and E as above. The distinction between Concept and NewConcept facilitates equivalence reviewing as described below. 4. Conjecture, in the form [conj:D1:D2:K], where D1 and D2 are concept definitions and K is a keyword indicating the type of conjecture. In this configuration, K is limited to being either im, which denotes that D1 is conjectured to imply D2; or eq, denoting D1 is conjectured to be equivalent to D2. 5. Explanation, in the form [exp:D1:D2:K:R:P], where D1, D2 and K represent a conjecture, as above. R is a keyword indicating the type of explanation; either true, which indicates that the conjecture has been proved, for example by a prover process; or false, where the conjecture has been refuted, for instance a model generator has found a counter-example. P gives details of the proof or refutation, as appropriate. An example Definition from quasigroup theory is [def:m(Q,A,A,B),m(Q,B,B,A)], which describes elements of quasigroups satisfying the equation A A = B ^ B B = A. The m=4 predicate defines the multiplication table for a quasigroup; e.g. m(Q0; 0; 1; 2) states that 0 1 = 2 for quasigroup instance Q0. The NewConcept artefact would be [new:m(Q,A,A,B),m(Q,B,B,A):((Q0,0,1),(Q0,1,0),(Q1,2,1),. . . )], with an associated example set. These are tuples of valid bindings for the definition variables; fQ0; Q1g are identifiers for different quasigroups and f0,1,2g are the elements of those quasigroups. The conjecture 8 A B (A B = B A $ A = B) would be represented as [conj:m(Q,A,B, C),m(Q,B,A, C):e(Q,A,B):eq], in a Conjecture artefact where the e/3 predicate, e(Q,A,B) is the equality of two elements within a particular algebra instance (A = B in quasigroup Q). A proof of this conjecture in an Explanation artefact would be as follows; [exp:m(Q,A,B, C),m(Q,B,A, C):e(Q,A,B):eq:true:proof text].
We make use of flags attached to broadcast artefacts to control the workspace. In particular, Definition and Concept artefacts have an attached complexity flag indicating the number of definitions, including itself, that have been used in creating that definition. This allows us to place an upper limit upon processing. For example, the definition m(Q,A,A,B),m(Q,B,B,A) would have a complexity of 3; in addition to itself, this definition has used the background definition of multiplication m(Q,A,B,C), and the concept of squaring an element m(Q,A,A,B). For clarity, we have omitted these flags from the formal definitions of the broadcasts, above. 3.2
We developed the following types of processes for use in the Quasigroup Theorem Discovery configuration: 1. DefinitionCreator processes propose new Definitions. They each encapsulate a different concept formation method, akin to production rules in HR. They react to NewConcept broadcasts, [new:D:E]. Some formation methods involve modifying a single concept definition, where they attempt to create a new definition from D. Others combine two definitions, in which case they remember D, by spawning a clone process that reacts to NewConcept broadcasts, [new:D’:E’:C’], by attempting to combine D and D’. 2. DefinitionReviewer, reacts to Definition broadcasts, [def:D], and removes redundancy by checking whether D has been seen before. If not, it proposes for broadcast [conc:D:0/ ], i.e. a concept with definition D and an empty example set. 3. ExampleFinder, encapsulates a Prolog database containing examples for the initial background concepts. All concept definitions are Prolog terms and ExampleFinder can generate example sets for new concepts by querying Prolog with the definition. ExampleFinder reacts to Concept broadcasts with empty example sets, [conc:D: 0/], by generating an example set E. If E is non-empty, it proposes [conc:D:E]. 4. EquivalenceReviewer, checks each new concept to identify and filter out those having the same example set as a previously developed concept. This removes a great deal of duplicated effort as the further development of each concept would give equivalent results. The process reacts to Concept broadcasts [conc:D:E] by proposing for broadcast [new:D:E]. Also, the process reacts to broadcast [new:D1:E1] by spawning a clone process P. For any future Concept broadcast [conc:D2:E2], if P finds that E2 = E1, it proposes an equivalence conjecture between them: [conj:D1:D2:eq]. A higher iportance value is allocated to equivalence conjecture proposals than to concept proposals. In the case where E2 = E1, both [conj:D1:D2:eq] and [new:D2:E2] will be proposed and the conjecture will be broadcast as it has higher importance. [new:D2:E2] will only be broadcast in the case where no spawned process identifies equivalence. 5. ImplicationMaker, compares the example sets of two NewConcept broadcasts. It reacts to the first NewConcept, [new:D1:E1], (where E1 6= 0/), by spawning a clone process, P, which itself reacts to future NewConcept broadcasts [new:D2:E2]. In particular, if P finds that E1 E2, it proposes [conj:D1:D2:im] (or [conj:D2:D1:im] if E2 E1). 6. Prover processes encapsulate the Prover9 theorem prover with axioms for the domain under investigation. It attempts to prove conjectures in any Conjecture broadcast, [conj:D1:D2:K], and proposes [exp:D1:D2:K:true:P], whenever a proof, P, is found.
The definition methods embodied by the DefinitionCreator processes are either unary or binary.
Unary methods act upon one definition. An example of a unary method is called variable freeing. Given
the starting concept m(Q; A; A; B), i.e., the arity 3 concept of pairs of elements for which A A = B,
freeing the variable A would result in the concept m(Q; A; A; B), which is the arity 2 concept of
elements B, which are the square of some element. In addition, there are unary concept forming processes
which unify variables, for example creating m(Q; A; A; A) from m(A; B;C; D). Other methods include
grounding, which involves variable instantiation, and methods combining definitions as conjunctions
with themselves with different variable orderings. The most common binary methods involve either
creating a conjunction of two previous definitions and unifying their variables in a particular manner,
or creating a conjunction of a previous concept and the negation of another previous concept. These
methods are inspired by HR’s concept formation methods, as described in [
DefinitionCreator processes spawn other processes to repeat-propose the definitions they create. This means that the definition is not forgotten if it is not immediately broadcast. Several other process types, for example the ImplicationMaker and Prover also use such an approach. This repetition addresses the question of residual memory, which is not really tackled by GWA theory. 3.3
At the start of a session, a number of processes are attached to the global workspace. Several DefinitionCreator processes are attached as they each embody a different definition creation method and allow us to develop a theory in different ways. We attach DefinitionCreator processes for each of the definition formation methods described above. In addition, we include several parameterisations of each method, whereby the same formation method operates upon different sub-sets of variables. In addition to the DefinitionCreator processes, we attach one instance of each of the other processes defined above. We also specified a process which proposes BackgroundConcept and BackgroundAxiom artefacts for the domain, which starts the theory formation session. 3.4
The framework requires that each proposal is given a numerical rating and it chooses the highest for broadcast. However, for the experiments described below, we used a simple scheme; Definitions are scored at 100, Concepts with no examples at 200, Concepts with examples at 250. Any NewConcept broadcasts are given the value 300 and Conjectures 400 meaning, in particular, equivalence Conjectures will get precedence over NewConcepts. Explanations are valued at 500. Having Explanations ranked the most highly ensures that any proved theorems are broadcast immediately, which seemed sensible given the purpose of the application – to discover proved theorems about quasigroups. In addition, we also experimented with using the complexity measure to further rank Definitions, whereby the base importance of 100 is reduced by the definition’s complexity. This means that simpler definitions are more likely to win the competition for broadcast. Not surprisingly, we have found that this produces simpler theories in step-limited sessions. There are many different rating schemes we could experiment with, and we plan to do so. 3.5
As mentioned previously, we want to compare the configured framework against the ICARUS system,
as described in [
As an illustrative example, we will describe how our system discovered and proved result (i) above. The background concepts we supplied were the multiplication operator m(Q,A,B,C) which states that A*B=C for A,B,C 2 Q; and equality e(Q,A,A) :- m(Q,A, , ), which states that all elements of Q are equal to themselves. The workspace was configured according to the initial state described above. Examples for the background concepts were given to the ExampleFinder and axioms for QG3 quasigroups to the Prover process. For clarity, by propose below, we mean that a process made and repeatedly proposed a proposal for broadcast. We also omit complexity information.
In a fairly early processing round, a Definition artefact for m(Q,A,B,C) was broadcast.
DefinitionReviewer reacted to this definition and confirmed that it was novel, thus proposing it in a Concept artefact
with no examples. In the next round, this was broadcast, and ExampleFinder reacted by obtaining
examples of the concept from its Prolog database and proposing a Concept with these examples.
EquivalenceReviewer reacted to the broadcast by proposing a NewConcept with that definition and this was
subsequently broadcast as the concept was not equivalent to any previous concept. EquivalenceReviewer
reacted again to this broadcast NewConcept by spawning a clone process to review future Concepts for
equivalence with m(Q,A,B,C). In that same round, the broadcast also triggered the DefinitionCreator
process encapsulating the Unify-[
The configuration described above was our second major attempt at getting the framework to achieve results comparable to ICARUS. Our first attempt generated many repeat broadcasts and therefore performed much unnecessary processing. The main reason for this was that the same concept was formed in a number of different ways. Also, there were instances where a chain of definition creation methods applied to a definition resulted in that same definition, creating many repetitive loops. This redundancy meant that the first system took 25,000 rounds (during an hour of running time) to produce the three interesting theorems above, found amongst 15,000 other conjectures. In response, we added the DefinitionReviewer process to stop the repetition. Later, we designed the EquivalenceReviewer and made the distinction between Concept and NewConcept, to remove equivalent concepts. The results from the final version of this configuration represent a vast improvement upon those early results. 4
One of the purposes of using computer algebra packages is to gain a better understanding of certain
mathematical functions, and the calculation of outputs for inputs can often lead to the formation of
conjectures about the function. With the HOMER system, we combined the HR machine learning system
with the Maple computer algebra package so that HR could automatically discover conjectures about
some user-supplied Maple functions. In [
To produce equivalent results to HOMER, using the GC framework, we built a second configuration on top of the one described above. We used the same importance rating scheme as before, but we changed the artefacts slightly and the processes slightly more. In overview, the new configuration effectively passes conjectures through a series of filters which halt the progress of the conjecture if it fails a test indicating that it will be uninteresting. In addition to filtering, we also wanted to mimic the way in which HOMER splits conjectures into smaller ones, e.g., an equivalence is split into two implication conjectures. To achieve the filtering and splitting through the normal workspace-process mechanism, we changed the Conjecture reasoning artefact to be of the form [conj:D1:D2:K:L]. Here, L is a number in f0,1,2,3g which indicates the level of conjecture filter through which the conjecture has passed. The levels are as follows: (0) indicates that the conjecture has not been split or filtered, (1) indicates that the conjecture has been split into implicates (2) indicates that the conjecture cannot be proven trivially from details of the background examples and function definitions (3) indicates that the conjecture still cannot be proven after considering some of the other conjectures the user has chosen as axioms – this rules out conjectures which are specialisations of some interesting conjectures identified by the user. All conjectures initially proposed by the processes spawned by EquivalenceReviewer and ImplicationMaker are assigned level 0.
When configuring the concept forming processes, we took into account the infinite nature of the number line. That is, in order to make empirically correct conjectures which relate concepts, the example generation must be sound, i.e., the generation of examples for two logically equivalent concepts should always result in the same finite example set. For efficiency purposes, we restricted our consideration to working just with the numbers 1 to 50, but this introduces some problems. For example, s (28) = 56, so, with no further information, the result of t(s (28)) cannot be calculated. We resolved this problem by storing background function values to cover a much larger range of integers whilst restricting the generation of examples to 1 to 50. We introduced the notion of a generator variable, which is one from which all other variables in a definition can be generated, by being the output from a function to which the inputs are known or can themselves be generated. All background concepts are supplied with relevant function input and output information, and the concept forming production rules use this to avoid inventing ambiguous definitions.
In addition to upgrading the concept forming processes, we made a few changes to some other existing processes. In particular, using the notion of generator variables, DefinitionReviewer was improved to also check definitions for empirical testability. In this configuration, it rejects those definitions for which example sets cannot be soundly generated. Also, we have enabled the ExampleFinder process to use the Maple computer algebra system to calculate examples for background concepts which represent number theory functions. Moreover, the ImplicationMaker process can now be given a minimum example set size, and if a concept has fewer examples than this threshold, no conjectures will be made for that concept. This stops the formation of conjectures such as t(a) = 1 $ s (a) = 1, as the concepts on both the left and right hand side are only satisfied by the number 1. For this configuration, we implemented two types of Prover process. The level 1 Prover reacts to level 1 conjectures using background examples and function definitions in proof attempts. In contrast, the level 2 Prover reacts to level 2 conjectures and attempts a proof using the same axioms together with axioms supplied by the user. In each case, the prover proposes an Explanation artefact if they are successful and a Conjecture artefact of one level higher if they fail.
We also added processes to split equivalence conjectures into two implications, and a method by which conjectures concerning concepts with small example sets – which are likely to be uninteresting – are avoided. In particular, we added these processes: RightConjectureSplitter and LeftConjectureSplitter The first of these processes reacts to level 0 Conjecture broadcasts (both im and eq) by proposing a level 1 im conjecture with the same definition list. LeftConjectureSplitter performs similarly, but reverses the members of the definition list, and only in response to eq conjectures. This procedure increases the overall number of conjectures but does lead to more pertinent conjectures, e.g., the non-obvious side of an equivalence conjecture.
ConjectureApplicability This reacts to a Concept with a small set of examples satisfying its definition. It proposes a conjecture that the given examples are the only ones possible for that definition. For example, it would propose [conj:sigma(A,1):e(A,1):eq] on seeing that 1 is the only number for which s (A) = 1. These conjectures prevent further development of these concepts in a similar manner to the EquivalenceReviewer. 4.1
As for the experiments with the HOMER system, we used the s (n), t(n) and isprime(n) background
functions together with the notion of equality. We ran the system to completion with a complexity limit
of 6. Under a similar experimental set up, as reported in [
Secondly, variable ordering accounted for some of the difference in the results. Our system
considered t(a) = b ^ s (b) = a ^ t(b) = b to be equivalent to s (a) = b ^ t(a) = a. Depending on how the
variables are ordered, the example sets of each can be written [[
On the other hand, our system produced a number of concepts that were not produced by HOMER. Some of these were ignored by HOMER for good reason, e.g., our system produced several concepts in the form s (a) = b ^ (9 c (s (b) = c))). Here, c indicates the existence of a functional result for sigma(b). Such formulae are uninteresting extensions to earlier concepts. However, other concepts produced by our system and not HOMER were valid and potentially interesting. It is difficult to determine why HOMER missed these concepts, and we are still investigating this. Looking instead at the conjectures made by the two systems, we note that our configuration created 669 level 1 conjectures, i.e., after splitting valid equivalence conjectures into implicates. The first filter – which excluded conjectures if they were provable from the background definitions – removed 331 conjectures, leaving 338. By comparison, the HOMER system created 137 conjectures, of which Otter proved 43, using the same methods, leaving 94. The main reason for the difference in these numbers is the relative number of concepts that the two systems produced, which naturally meant that the configured framework produced more conjectures.
In a similar manner to that adopted for HOMER, we reviewed the 338 remaining conjectures. In particular, we looked at the first 10 conjectures and added the following as axioms (after re-combining some of the split implications): 8 a (s (a) = 1 ! a = 1) 8 a (t(a) = 1 ! a = 1) 8 a (t(a) = 2 $ isprime(a)) 8 a (s (a) = a $ s (a) = 1) 8 a (t(a) = a ! (a = 1ja = 2)) After running the process again, our configuration filtered out all but 66 conjectures (a reduction of around 90%). A similar kind of reduction was achieved by the users of HOMER, hence we can claim that our configured generic framework is capable of producing comparable results to the bespoke, ad-hoc HOMER system. Importantly, the most interesting (proved by hand) result from the HOMER experiments was: isprime(s (a)) ! isprime(t(a)), which our system re-discovered.
In addition to showing that our Global Workspace approach can be used to re-implement existing
combinations of reasoning systems, we can also use the system for novel applications, one of which we
describe here. In finite algebra, it is common for a specialisation of an algebra to be studied in its own
right, for instance, Cyclic groups, Abelian quasigroups [
The GC configuration for this application was similar to that used for quasigroup theorem discovery above, with a small number of amendments. Firstly, we introduced a MaceAxiomPopulator process, which uses the Mace model generator to produce background concepts and examples for the domain. The process reacts to the broadcast of a BackgroundAxiom by generating models for that axiom up to a user defined algebra size limit. It extracts the algebra operators from the models and generates example sets for them by interpreting the models. It then proposes these operators and examples sets together as a BackgroundConcept artefact, which initiates theory formation as before. This new process allows us to perform theory formation with only the axioms of the domain as a starting point. This greatly improves efficiency as, previously, a user was required to generate examples independently and convert them into an appropriate format. Our next amendment was to configure the system with two Prover processes; one of which uses the axioms of the domain in attempts to prove conjectures and another which holds no axioms. If this second prover can prove a conjecture then we know it is trivially true. This allows us to distinguish, potentially, more interesting conjectures. If the trivial prover can prove a conjecture then we know that the Prover with the domain axioms will also be able to prove it. Consequently, we weight the importance rating scheme toward the trivial proofs to ensure they are broadcast. We also introduced a MaceRefuter process which appeals to Mace to find counter-examples to broadcasts conjectures. This refutation process has access to higher orders of algebra and so can sometimes refute conjectures that have been generated by being empirically true for smaller orders.
Starting with a fairly unstructured algebraic domain such as quasigroup theory, we used the system to
generate 100 concepts which can be interpreted as specialisations, expressed in a Prolog style in terms of
the multiplication operator only. Then, for each specialisation, we started GC with the original axioms of
the algebraic domain, with the specialisation definition also added as an axiom. We then ran the system
until it generated and proved 100 implication theorems, and recorded the average length of the proof
produced by the Prover9 prover. In Table 1, we present the top ranked specialisations from three domains:
semigroups, quasigroups and star algebras (which have the single axiom: 8x; y; z((x y) z = y (z x)),
see [
Bearing in mind that the balance of syntactic simplicity and semantic complexity is often regarded as a maxim in pure mathematics – for instance, consider Fermat’s Last Theorem, which is very easily stated, but very difficult to prove – we looked for a specialisation of each algebra which had a high rank, yet a low complexity for its definition. In each case, we found suitable candidates. In particular, for semigroups, the specialisation (m(A, B, C, B)),n+(m(A, C, D, B)) has a definitional complexity of only 5 (it has three free variables, namely B, C and D, and two occurrences of the multiplication operator), but it is ranked 92nd out of the 100 specialisations, as it produces a theory with a proof length of 6.54 on average (with the best achieved being 7.76). The definition describes the notion of semigroups for which an element is the right identity of an element that does not appear on its row of the multiplication table. For quasigroups, the specialisations ranked 94th and 100th each have short definitions with a complexity of 7. The 100th ranked is ((m(A, B, C, C),m(A, D, D, D)),n+(m(A, E, E, B))), which alludes to the notion proof length, comp. is the sum of the variable and predicate counts. of quasigrioups having at least one idempotent element , and an element which is the left identity of some element but does not appear on the central diagonal of the multiplication table ,i.e. it is not the square of some other element. This specialisation produced the theory with the highest average proof length of 9.61. Interestingly, the specialisation ranked 94th is very similar to the 100th but describing an element that is a right identity. For star algebras, the 97th ranked specialisation is interesting. It represents a specialisation for which an implication should hold. Namely, for all elements x and y, if x y = x then y y = x. We further investigated this specialisation by drawing a graph to indicate how it relates to the other star algebra specialisations. In figure 1, the arrows all indicate an implication conjecture/theorem that the algebras satisfying the definition of the first specialisation all satisfy the definition of the second specialisation. Solid arrows are all true, i.e., can be proved from the background axioms. The arrows with a dotted line are only empirically true, i.e., Prover9 could not prove the implications, and MACE could not find counterexamples, even when we re-ran them for several minutes. These are therefore interesting open conjectures and we will continue to investigate them.
We have used the cognitive science theory of the Global Workspace Architecture (GWA) to devise and implement a generic computational framework within which disparate reasoning systems can be fruitfully combined. We have shown how the framework can be configured in order to achieve similar results to the ICARUS and HOMER combined reasoning systems which were implemented in an ad-hoc way for specific purposes. We have also demonstrated a novel application of a configuration of our system to investigating algebra specialisations. We applied this system to three classes of finite algebra and, in each case, it identified a syntactically simple, although semantically quite complex, specialisation of that algebra that may be worthy of further mathematical investigation.
While the value of using disparate AI systems in combination has been repeatedly demonstrated, the combined reasoning systems themselves are in general ad-hoc and purpose-specific. We believe that in order for the field of combined reasoning to progress, there needs to be much more research into generic frameworks within which different AI problem solving methods can be integrated. We hope that the framework presented here will eventually become one of many that researchers can turn to when they need to harness the power of more than one reasoning approach in combination.
While the functionality that the framework provides is fairly straightforward, we have shown that it is
possible to configure it to achieve behaviour which combines induction, deduction and calculation.
Producing similar results to those of previous ad-hoc systems has been the first milestone in the development
and testing of the framework. We intend to further demonstrate the potential of the system by adding
constraint solving processes, so that the full functionality of the ICARUS system can be achieved. We
will further add model generation, SAT-solving and planning processes so that results similar to those
from other combined reasoning systems – in particular the TM system [
While much of our effort to date has been spent on writing processes which achieve theory formation like the HR system, it is important to note how differently the configured frameworks presented here perform when compared to the very linear approach in HR. In particular, one of the potential benefits of a framework based on the Global Workspace Architecture is the ability to distribute the reasoning it performs over many processors. We plan to implement a distributed version of the framework, and to determine the efficiency gains to be made.
Currently, our framework operates in a synchronous manner, where all processes are given time to react before a new round is begun. Relaxing this requirement may yield efficiency gains as some processes react much faster than others. It may be possible, for instance, for the reasoning to proceed for many rounds while a difficult theorem is proved on one processor. Furthermore, all processes are given equal resources, and these could be adapted based upon perceived difficulty or importance of a particular process’ task. We have only scratched the surface of the experimental possibilities that the framework provides.
We chose quite straightforward importance rating schemes for the two configurations in order to achieve similar results to HOMER and ICARUS. However, it is not clear that these are the best possible schemes. In our experience with the HR system, it often pursues avenues of a theory which ultimately lead to little of interest. It will be interesting for us to experiment with different setups of processes and schemes to see which configurations of the framework are more fruitful, or which solve problems more efficiently. We have only touched upon grading importance based upon the specifics of a proposal. We could extend the sophistication of processes so that they consider other factors such as previous broadcasts by other processes or by specialist control processes. This could also encompass such things as information from the user or some external guiding system giving real-time feedback about the progress of the system.
In addition to using the framework to advance the field of combining reasoning systems, we hope to use it to shed light on the area of Global Workspace Architectures. We have already had to deviate on two occasions from the standard theory of the GWA, in particular by allowing processes to terminate themselves and to add new processes to the workspace. With a computational model of the GWA, we hope to make the theory more concrete and more useful as a tool both for cognitive scientists and AI researchers. 7