China 
Africa 
Explore chapters and articles related to this topic
Introduction to Expert Systems
Published in Chris Nikolopoulos, Expert Systems, 1997
Green introduced a method to retrieve the unification bindings that took place during the proof of a theorem, in effect giving the theorem proving system a query answering capability, ([7]). This is accomplished by appending an extra disjunction to the negated theorem, the answer term, containing all the variables whose values we want to retrieve.
Formal Methods
Published in Cary R. Spitzer, Uma Ferrell, Thomas Ferrell, Digital Avionics Handbook, 2017
Key characteristics of the DO-333 analysis categories mentioned earlier can be summarized as follows: Deductive techniques establish the truth of explicitly stated properties using a theorem-proving system. Properties are typically expressed in the same notation as the formal models. Theorem provers can be either automatic or interactive. In both cases, users need to understand the underlying logical formalism to construct proofs effectively.Model checking makes use of efficient exploration of large state spaces to verify properties of formal models. Most models are based on state transition systems of various kinds. An important tool feature is the ability to generate counterexamples or other diagnostic information in response to failed verification attempts.Abstract interpretation relies on formalized semantics of programming languages to analyze properties over abstract domains. The technique is normally realized through sound algorithms that examine source code to ascertain whether various predefined properties hold. Tools usually take the form of static analyzers for mainstream programming languages.
A Creativity Support System Based on Causal Mapping
Published in Journal of Computer Information Systems, 2018
This issue, the evaluation of novel ideas, is indeed one of the major problems faced by the research in computational creativity, as it is always problematic to assess the outputs of the system in terms of creative contribution (as it is difficult, in general, to assess the creativity of a person). This issue has been addressed by Colton [15], who developed a system in which a conjecture generation model, HR [16], interacts with a theorem proving system, Otter [51], in order to discard the conjectures produced by HR that are trivial for the Otter to prove. The HR has information about the domain studied, including objects of interest, initial concepts, and examples. The HR is able to build new concepts and to make conjectures [15, 16]. Colton’s HR has been extended by Pease et al. [56] to allow the production of conjectures with known counterexamples, to include the analysis of faulty conjectures, and to use a multi-agent approach in which agents are able to request and communicate with each other. Under this approach, the threshold considered to assess novelty is the one of discarding trivial conjectures. Hence, novel ideas are not creative if they do not pass this minimum threshold.