Explore chapters and articles related to this topic
Logic
Published in Jay Liebowitz, The Handbook of Applied Expert Systems, 2019
Logic can be studied with respect to ontological and epistemological commitments. Ontological commitments have to do with what is assumed to exist in the world; thus, propositional logic assumes that the world consists of facts that are either true or false. First-order logic assumes that the world consists of objects with relationships among them that either hold or do not hold; quantification is made only on objects. Higher-order logic assumes that the world is made of objects, categories of objects, and relationships among them; quantification is made over objects, predicates, and functions. Epistemological commitments have to do with the possible states of knowledge owned by an intelligent system. A system that represents knowledge using propositional, first-order, or higher-order logic believes a formula that represents a fact about the world to be true, to be false, or it could be unable to conclude either way. Systems that represent uncertain knowledge using probability theory, on the other hand, can have any degree of belief, typcially rendered as numbers in the range 0 (e.g., “total disbelief”) to 1 (e.g., “total belief”). Systems that represent uncertain knowledge using fuzzy logic can have degrees of belief in a sentence like probabilistic systems, but their ontological commitment assumes that what exists does so with associated degrees of truth.
Formal Methods
Published in Cary R. Spitzer, Uma Ferrell, Thomas Ferrell, Digital Avionics Handbook, 2017
PVS was introduced by SRI International in 1992. It features an interactive theorem prover for a typed form of classical higher-order logic. The specification language, also called PVS, is based on a syntax similar to modern programming languages. The PVS user interface is implemented using the Emacs text editor as a front end to the proof system. Through the Emacs interface, users manage and edit files, submit analysis and verification commands, and carry out all other system interactions including interactive proving. PVS is available from SRI International as open-source software.
Algebra for Enterprise Ontology: towards analysis and synthesis of enterprise models
Published in Enterprise Information Systems, 2018
DEMO is equipped with a formalization, the CRISP model, which is described as a meta model for modeling organizations (Dietz 2006, 217). In CRISP, a DEMO model, originated by an elementary or composite actor role, is formalized by a 5-tuple 4 in the form of a finite automaton (Dietz 2015). According to the CRISP meta model, a model of an elementary organization is called a crispie and an organization is modeled as a crispienet, a network of collaborating crispies (Dietz 2006, 133). Therefore, allying multiple crispies into one crispienet is regarded as model manipulation in the terminology of this research. Although the CRISP model initially appears to be a good approach for formalizing DEMO models, these formalizations are too complex to define operations over because manipulation over crispies, which is substantially equal to function over the performance functions, will be a higher-order function (taking functions as arguments). It requires not only advanced mathematics but also model theory for a higher order logic, which is not developed very well. Based on CRISP, model manipulations must be formulated as operations over mappings. Therefore, CRISP is not suitable for this research.