Search

Fault Scenario Identification (FSI) is a challenging task that aims to automatically identify the fault types in communication networks from massive alarms to guarantee effective fault recoveries. Existing methods are developed based on rules, which are not accurate enough due to the mismatching issue. In this paper, we propose an effective method named Knowledge-Enhanced Graph Neural Network (KE-GNN), the main idea of which is to integrate the advantages of both the rules and GNN. This work is the first work that employs GNN and rules to tackle the FSI task. Specifically, we encode knowledge using propositional logic and map them into a knowledge space. Then, we elaborately design a teacher-student scheme to minimize the distance between the knowledge embedding and the prediction of GNN, integrating knowledge and enhancing the GNN. To validate the performance of the proposed method, we collected and labeled three real-world 5G fault scenario datasets. Extensive evaluation conducted on these datasets indicates that our method achieves the best performance compared with other representative methods, improving the accuracy by up to 8.10%. Furthermore, the proposed method achieves the best performance against a small dataset setting and can be effectively applied to a new carrier site with a different topology structure.

It is widely assumed that there exist mismatches between the connectives of Propositional Logic and their counterparts in Natural Language. One mismatch that has been extensively discussed is Conditional Perfection, the phenomenon in which a conditional sentence is interpreted as a biconditional under some circumstances. The Pragmatics literature has provided valuable insights into the question of whether Conditional Perfection will happen in a given context. In order to make these insights more explicit and testable, we designed an algorithm to generate pragmatically more appropriate sentences from propositional logical formulas involving material implication and biconditional implication. This algorithm was tested in an evaluation by human participants, in which generated sentences are compared against those generated by a simple baseline algorithm. The evaluation results suggest that the designed algorithm generates better sentences, which capture the semantics of the logical formulas more faithfully.

Some logics make it easier to say what we want than others and some methods of deduction are simpler to work with than others. One thing typically remains important: that we can deduce all valid things (completeness). In this thesis I tackle completeness of various deduction methods for various logics. The work is formalized in the proof assistant Isabelle/HOL which offers a common language for mathematics and computer science where proofs can be checked mechanically. This thesis discusses the following contributions of my PhD project in particular: • A historical overview of formalized completeness proofs and a formalization that explains the essence of synthetic completeness proofs. • A formalization of a concise completeness proof for first-order logic in Isabelle/HOL, including solutions to the issues of formalizing quantifiers and proving completeness for formulas with free variables. • A verified prover for first-order logic with functions, with a formalized completeness proof that takes the search strategy of the prover into account. • A synthetic completeness proof for a tableau system for basic hybrid logic which is both terminating and in the Seligman style where the proof rules reflect the local perspective that modal logic is based on. • Formalized soundness and completeness results for epistemic and public announcement logic, instantiated to a range of concrete axiom systems. • A best-first proof search tactic for the proof assistant Lean 4. • An abstract framework for synthetic completeness proofs.

Delftse Foundations of Computation is a textbook for a one quarter introductory course in theoretical computer science. It includes topics from propositional and predicate logic, proof techniques, set theory and the theory of computation, along with practical applications to computer science. It has no prerequisites other than a general familiarity with computer programming., TU Delft OPEN Textbook, Data-Intensive Systems, Algorithmics

Automated reasoning is the study of computer programs that can build proofs of theorems in a logic. Such programs can be either automatic theorem provers or interactive theorem provers. The latter are also called proof assistants because the user constructs the proofs with the help of the system. We focus on the Isabelle proof assistant. The system ensures that the proofs are correct, in contrast to pen-and-paper proofs which must be checked manually. We present applications to logical systems and models of information, in particular selected modal logics extending classical propositional logic. Epistemic logic allows intelligent systems to reason about the knowledge of agents. Public announcements can change the knowledge of the system and its agents. In order to account for this, epistemic logic can be extended to public announcement logic. An axiomatic system consists of axioms and rules of inference for deriving statements in a logic. Sound systems can only derive valid statements and complete systems can derive all valid statements. We describe formalizations of sound and complete axiomatic systems for epistemic logic and public announcement logic, thereby strengthening the foundations of automated reasoning for logic and information.

This paper describes LOGAX, an interactive tutoring tool that gives hints and feedback to a student who stepwise constructs a Hilbert-style axiomatic proof in propositional logic. LOGAX generates proofs to calculate hints and feedback. We compare these generated proofs with expert proofs and student solutions, and conclude that the quality of the generated proofs is comparable to that of expert proofs. LOGAX recognizes most steps that students take when constructing a proof. Even if a student diverges from the generated solution, LOGAX still provides hints, including next steps or reachable subgoals, and feedback. With a few improvements in the design of the set of buggy rules, LOGAX will cover about 80% of the mistakes made by students by buggy rules. The hints help students to complete the exercises.

We formalize soundness and completeness proofs for a number of axiomatic systems for propositional logic in the proof assistant Isabelle/HOL.

We formalize a Henkin-style completeness proof for an axiomatic system for propositional logic in the proof assistant Isabelle/HOL. Our formalization precisely details the structure of this proof method.

Provability in the intuitionistic second-order propositional logic (resp. inhabitation in the polymorphic lambda-calculus) was shown by Löb to be undecidable in 1976. Since the original proof is heavily condensed, Arts in collaboration with Dekkers provided a fully unfolded argument in 1992 spanning approximately fifty pages. Later in 1997, Urzyczyn developed a different, syntax oriented proof. Each of the above approaches embeds (an undecidable fragment of) first-order predicate logic into second-order propositional logic. In this work, we develop a simpler undecidability proof by reduction from solvability of Diophantine equations (is there an integer solution to P(x_1, ..., x_n) = 0 where P is a polynomial with integer coefficients?). Compared to the previous approaches, the given reduction is more accessible for formalization and more comprehensible for didactic purposes. Additionally, we formalize soundness and completeness of the reduction in the Coq proof assistant under the banner of "type theory inside type theory".

Purpose In the field of crime prevention there are several theoretical approaches explaining why crime occurs and how to prevent it. Three of them – routine activity theory, crime pattern theory and the theory of crime-as-choice – are logically tested in this work. The point of departure is to test if the theories are logical consistent and logical valid, irrespective of whether the criterion for criminal intent is changed from direct intention to negligence. Design/methodology/approach The issues will be explored in a logical structure by a first-order logic propositional analysis. Findings The analysis shows that all three theories are logical consistent, but only routine activity theory is logical valid. The conclusion is that crime prevention should in general assume that routine activity theory is the legitimate theory and that social prevention as a prevention strategy is logically unnecessary to adopt because it does not matter whether the offender is motivated (direct intention) or not (negligence). Practical implications It does not really matter if the authors theoretically treat white-collar offenders as motivated, because if they have committed an actus reus, they are an offender according to the objective requisites. This means that the best strategies to prevent a potential white-collar criminal are situational prevention, i.e. complicate their access to money, where it becomes irrelevant if the potential offender has a mens rea or not. What counts is the prevention of actus reus by a potential offender. Originality/value As far as I know, no one has previously investigated the logical consistency and/or logical validity of routine activity theory, crime pattern theory and the theory of crime-as-choice as theories of crime prevention.

This is a companion to a paper by the authors entitled "Godel on deduction", which examined the links between some philosophical views ascribed to Godel and general proof theory. When writing that other paper, the authors were not acquainted with a system of natural deduction that Godel presented with the help of Gentzen's sequents, which amounts to JaA gt kowski's natural deduction system of 1934, and which may be found in Godel's unpublished notes for the elementary logic course he gave in 1939 at the University of Notre Dame. Here one finds a presentation of this system of Godel accompanied by a brief reexamination in the light of the notes of some points concerning his interest in sequents made in the preceding paper. This is preceded by a brief summary of Godel's Notre Dame course, and is followed by comments concerning Godel's natural deduction system.

This paper describes an algorithm to generate Hilbert-style axiomatic proofs. Based on this algorithm we develop logax, a new interactive tutoring tool that provides hints and feedback to a student who stepwise constructs an axiomatic proof. We compare the generated proofs with expert and student solutions, and conclude that the quality of the generated proofs is comparable to that of expert proofs. logax\ recognizes most steps that students take when constructing a proof. If a student diverges from the generated solution, logax can still provide hints and feedback.

The research is it proposed to demonstrate that the application of the problem-solving method improves the academic performance in the mathematical logic subject of the students of the first cycle, Faculty of Sciences of the Education and Social Communication; National University Daniel Alcides Carrion, Peru. We used the scientific method, the quasi-experimental design with pretest and posttest, validated with expert judgment methodology and reliability with split halves methodology; the results showed a significant improvement of the experimental group with respect to the control group; the Student's T-test was used to conclude the validation of the research hypothesis., La investigación se propuso demostrar que la aplicación del método de resolución de problemas mejora el rendimiento académico en la asignatura lógica matemática de los estudiantes del primer ciclo, Facultad de Ciencias de la Educación y Comunicación Social; Universidad Nacional Daniel Alcides Carrión, Perú. Se usó un diseño cuasi experimental con pretest y post test, validados con metodología del juicio de expertos y la confiabilidad con metodología de mitades partidas; los resultados demostraron mejora significativa del grupo experimental respecto al grupo control; se usó la prueba T-Student que permitió concluir la validación de la hipótesis de investigación.

The modal characterization theorem by J. van Benthem characterizes classical modal logic as the bisimulation invariant fragment of first-order logic. In this paper, we prove a similar characterization theorem for intuitionistic modal logic. For this purpose we introduce the notion of modal asimulation as an analogue of bisimulations. The paper treats four different fragments of first-order logic induced by their respective versions of Kripke-style semantics for modal intuitionistic logic. It is shown further that this characterization can be easily carried over to arbitrary first-order definable subclasses of classical first-order models. © 2016 Elsevier B.V.

The computational properties of modal and propositional dependence logics have been extensively studied over the past few years, starting from a result by Sevenster showing NEXPTIME-completeness of the satisfiability problem for modal dependence logic. Thus far, however, the validity and entailment properties of these logics have remained uncharacterised to a great extent. This paper establishes a complete classification of the complexity of validity and entailment in modal and propositional dependence logics. In particular, we address the question of the complexity of validity in modal dependence logic. By showing that it is NEXPTIME-complete we refute an earlier conjecture proposing a higher complexity for the problem.

We rethink the way Natural Deduction systems are usually used in logic, and adapt them in order to solve the MaxSAT problem. By adapting some existing rules and defining some new ones, the Natural Deduction method can be used to provide an elegant and straightforward solution to maximum satisfiability problems of multisets of Boolean and many-valued clauses. © 2017 The authors and IOS Press. All rights reserved.

This paper describes an algorithm to generate Hilbert-style axiomatic proofs. Based on this algorithm we develop logax, a new interactive tutoring tool that provides hints and feedback to a student who stepwise constructs an axiomatic proof. We compare the generated proofs with expert and student solutions, and conclude that the quality of the generated proofs is comparable to that of expert proofs. logax recognizes most steps that students take when constructing a proof. If a student diverges from the generated solution, logax can still provide hints and feedback.

Psychologists and cognitive scientists have long drawn insights and evidence from stage magic about human perceptual and attentional errors. We present a complementary analysis of conjuring tricks that seeks to understand the experience of impossibility that they produce. Our account is first motivated by insights about the constructional aspects of conjuring drawn from magicians' instructional texts. A view is then presented of the logical nature of impossibility as an unresolvable contradiction between a perception-supported belief about a situation and a memory-supported expectation. We argue that this condition of impossibility is constructed not simply through misperceptions and misattentions, but rather it is an outcome of a trick's whole structure of events. This structure is conceptualized as two parallel event sequences: an effect sequence that the spectator is intended to believe; and a method sequence that the magician understands as happening. We illustrate the value of this approach through an analysis of a simple close-up trick, Martin Gardner's Turnabout. A formalism called propositional dynamic logic is used to describe some of its logical aspects. This elucidates the nature and importance of the relationship between a trick's effect sequence and its method sequence, characterized by the careful arrangement of four evidence relationships: similarity, perceptual equivalence, structural equivalence, and congruence. The analysis further identifies two characteristics of magical apparatus that enable the construction of apparent impossibility: substitutable elements and stable occlusion.

An important topic in courses in propositional logic is rewriting propositional formulae with standard equivalences. This paper analyses what kind of feedback is offered by the various learning environments for rewriting propositional logic formulae, and discusses how we can provide these kinds of feedback in a learning environment. To give feedback and feed forward, we define solution strategies for several classes of exercises. We offer an extensive description of the knowledge necessary to support solving this kind of propositional logic exercises in a learning environment.

This is a companion to a paper by the authors entitled "Godel's natural deduction," which presented and made comments about the natural deduction system in Godel's unpublished notes for the elementary logic course he gave at the University of Notre Dame in 1939. In that earlier paper, which was itself a companion to a paper that examined the links between some philosophical views ascribed to Godel and general proof theory, one can find a brief summary of Godel's notes for the Notre Dame course. In order to put the earlier paper in proper perspective, a more complete summary of these interesting notes, with comments concerning them, is given here.

We study quantified propositional logics from the complexity theoretic point of view. First we introduce alternating dependency quantified boolean formulae (ADQBF) which generalize both quantified and dependency quantified boolean formulae. We show that the truth evaluation for ADQBF is AEXPTIME(poly)-complete. We also identify fragments for which the problem is complete for the levels of the exponential hierarchy. Second we study propositional team-based logics. We show that DQBF formulae correspond naturally to quantified propositional dependence logic and present a general NEXPTIME upper bound for quantified propositional logic with a large class of generalized dependence atoms. Moreover we show AEXPTIME(poly)-completeness for extensions of propositional team logic with generalized dependence atoms.

LogEx is a learning environment that supports students in rewriting propositional logical formulae, using standard equivalences. We organized a pilot study to prepare a large scale evaluation of the learning environment. In this paper we describe this study, together with the outcomes, which teach us valuable lessons for the large scale evaluation.

We give sound and complete Hilbert-style axiomatizations for propositional dependence logic (PD), modal dependence logic (MDL), and extended modal dependence logic (EMDL) by extending existing axiomatizations for propositional logic and modal logic. In addition, we give novel labeled tableau calculi for PD, MDL, and EMDL. We prove soundness, completeness and termination for each of the labeled calculi.

Recently it has been observed that the set of all sound linear inference rules in propositional logic is already coNP-complete, i.e. that every Boolean tautology can be written as a (left- and right-) linear rewrite rule. This raises the question of whether there is a rewriting system on linear terms of propositional logic that is sound and complete for the set of all such rewrite rules. We show in this paper that, as long as reduction steps are polynomial-time decidable, such a rewriting system does not exist unless coNP=NP. We draw tools and concepts from term rewriting, Boolean function theory and graph theory in order to access the required intermediate results. At the same time we make several connections between these areas that, to our knowledge, have not yet been presented and constitute a rich theoretical framework for reasoning about linear TRSs for propositional logic.

Belief merging is a relatively recent technique with the aim of combining pieces of infor- mation, possibly inconsistent, coming from different sources. This process is done by a merging operator, in the literature we found mainly the theoretical basis of operators. However, this technique is still little known and there is scarce evidence about its applicability to solve real-world problems. In this paper we propose to use belief merging in order to solve everyday decision-making problems, in which participants with the same level have contradictory opinions, by \merging" these opinions and generating a common non-contradictory opinion representing the views of the majority.We describe in detail three belief merging operators with differing properties: , GMax , y ps (PS-Merge); afterwards, the classic belief merging examples are presented in natural language as decision-making practical scenarios; finally, we present an online open source Belief Merging Prototype to support on diverse decision-making processes., La fusión de creencias es una técnica relativamente reciente que permite combinar piezas de información, posiblemente contradictorias, provenientes de diferentes fuentes. Este proceso lo realiza un operador de fusión, en la literatura se describen principalmente los fundamentos teóricos de los operadores. Sin embargo, la fusión de creencias es en general poco conocida y existe escasa evidencia de su aplicabilidad para resolver problemas de la vida diaria. En este artículo se propone emplear esta técnica para solucionar problemas relacionados con la toma de decisiones en escenarios cotidianos, donde los involucrados poseen opiniones contradictorias y tienen el mismo nivel jerárquico, \fusionando" estas opiniones y generando una opinión conjunta sin contradicciones que representa la opinión de la mayoría. Se describen a detalle tres operadores de fusión de creencias con diferentes características: , GMax , y ps (PS-Merge); posteriormente los ejemplos clásicos de fusión de creencias se representan en lenguaje natural empleando escenarios prácticos, donde se involucra la toma de decisiones; finalmente para apoyar en la toma de decisiones de diversa índole se presenta un Prototipo Fusionador de Creencias bajo licencia libre, disponible en línea.

Linear inferences are sound implications of propositional logic where each variable appears exactly once in the premiss and conclusion. We consider a specific set of these inferences, MS, first studied by Straßburger, corresponding to the logical rules in deep inference proof theory. Despite previous results characterising the individual rules of MS, we show that there is no polynomial-time characterisation of MS, assuming that integers cannot be factorised in polynomial time. We also examine the length of rewrite paths in an extended system MSU that also has unit equations, utilising a notion dubbed trivialisation to reduce the case with units to the case without, amongst other observations on MS-rewriting and the set of linear inferences in general.

This article was presented at a conference (entitled 'Mistakes of Reason') in honour of John Woods held at the University of Lethbridge, April 19–21, 2002. Some corrections and additions were made in November 2012, in response to annotations by Erik Krabbe, for which I am grateful to him. Part of this paper formed the basis of my chapter entitled ‘The peculiarities of Stoic logic’ in Andrew D. Irvine and Kent A. Peacock, eds., Mistakes of Reason: Essays in Honour of John Woods (Toronto: University of Toronto Press, 2006), 224-242., I reconstruct Stoic propositional logic, from the ancient testimonies, in a way somewhat different than the 10 reconstructions published before 2002, building especially on the work of Michael Frede (1974) and Suzanne Bobzien (1996, 1999). In the course of reconstructing the system, I draw attention to several of its features that are rarely remarked about, such as its punctuation-free notation, the status of the premisses of an argument as something intermediate between a set and a sequence of propositions, the incorrectness of the almost universal translation of the Greek label for the primitives of the system as indemonstrable arguments, the probable existence of an extended set of primitives which accommodates conjunctions with more than two conjuncts and disjunctions with more than two disjuncts, the basis for the system’s exclusion of redundant premisses, and the reason why the hypothetical syllogisms of Theophrastus are not derivable in the system. I argue that, though sound according to its originator’s (Chrysippus’s) conception of validity, the system as reconstructed is not complete according to that conception. It is an open problem what one needs to add to the system in order to make it Chrysippean-complete, or even whether it is possible to do so without making it Chrysippean-unsound.

General introduction to logic, with emphasis on epistemic logic and logical analysis of games

A pool resolution proof is a dag-like resolution proof which admits a depth-first traversal tree in which no variable is used as a resolution variable twice on any branch. The problem of determining whether a given dag-like resolution proof is a valid pool resolution proof is shown to be NP-complete.

This paper addresses the problem of the acquisition of the syntax of propositional logic. An approach based on general purpose cognitive capacities such as invention, adoption, parsing, generation and induction is proposed. Self-organisation principles are used to show how a shared set of preferred lexical entries and grammatical constructions, i.e., a language, can emerge in a population of autonomous agents which do not have any initial linguistic knowledge. Experiments in which a population of autonomous agents constructs a grammar that allows communicating the formulas of a propositional logic language are presented. These experiments extend previous work by considering a larger population and a much larger search space of grammar rules. In particular the agents are allowed to order the expressions associated with the constituents of a logical formula in arbitrary order. Previous work assumed that the expressions associated with the connectives should be placed in the first position of the sentence., Peer Reviewed, Postprint (author’s final draft)

Ve své bakalářské práci se zabývám problematikou výrokové a predikátové logiky. První část práce by měla čtenáře seznámit s významem této části matematiky a s jejími základními pojmy. Druhá část práce se věnuje architektuře výukového pro-gramu, který obsahuje kromě samotné teorie také test a který bude sloužit studentům pro domácí opakování znalostí výrokové a predikátové logiky., In my baccalaureate work deal with problems propositional and predicate logic. First volume of work would had reader acquaint with meaning those parts mathematics and with her basic notions. Alternative volume of work paies architecture tutorial, that contains except himself theory also test and will be of service students for native repetition knowledge dictum and predicate logic., Katedra informačních technologií, Dokončená práce s úspěšnou obhajobou

The system cc ⊤ is a tool for testing correspondence between propositional logic programs under the answer-set semantics with respect to different refined notions of program correspondence. The underlying methodology of cc ⊤ is to reduce a given correspondence problem to the satisfiability problem of quantified propositional logic and to employ extant solvers for the latter language as back-end inference engines. In a previous version of cc ⊤, the system was designed to test correspondence between programs based on relativised strong equivalence under answer-set projection. Such a setting generalises the standard notion of strong equivalence by taking the alphabet of the context programs as well as the projection of the compared answer sets to a set of designated output atoms into account. This paper outlines a newly added component of cc ⊤ for testing similarly parameterised correspondence problems based on uniform equivalence.

In recent work, a general framework for specifying program correspondences under the answer-set semantics has been defined. The framework allows to define different notions of equivalence, including the well-known notions of strong and uniform equivalence, as well as refined equivalence notions based on the projection of answer sets, where not all parts of an answer set are of relevance (like, e.g., removal of auxiliary letters). In the general case, deciding the correspondence of two programs lies on the fourth level of the polynomial hierarchy and therefore this task can (presumably) not be efficiently reduced to answer-set programming. In this paper, we give an overview about an implementation to compute program correspondences in this general framework. The system, called eqcheck, relies on linear-time constructible reductions to quantified propositional logic using extant solvers for the latter language as back-end inference engines. We provide some preliminary performance evaluation, which shed light on some crucial design issues.

In recent work, a general framework for specifying correspondences between logic programs under the answer-set semantics has been defined. The framework captures different notions of equivalence, including well-known ones like ordinary, strong, and uniform equivalence, as well as refined ones based on the projection of answer sets where not all parts of an answer set are of relevance. In this paper, we describe an implementation to verify program correspondences in this general framework. The system, called ccT, relies on linear-time constructible reductions to quantified propositional logic and uses extant solvers for the latter language as back-end inference engines.

This course surveys a variety of reasoning, optimization, and decision-making methodologies for creating highly autonomous systems and decision support aids. The focus is on principles, algorithms, and their applications, taken from the disciplines of artificial intelligence and operations research. Reasoning paradigms include logic and deduction, heuristic and constraint-based search, model-based reasoning, planning and execution, reasoning under uncertainty, and machine learning. Optimization paradigms include linear, integer and dynamic programming. Decision-making paradigms include decision theoretic planning, and Markov decision processes. This course is offered both to undergraduate (16.410) students as a professional area undergraduate subject, in the field of aerospace information technology, and graduate (16.413) students.

I develop a new model of sequential decision processes over multiple interconnected propositions, combining social choice theory and propositional logic. I focus on so-called priority-to-the-past decision processes. A sequential decision over multiple propositions is path-dependent if its outcome depends on the order in which the propositions are considered. I prove three main results. (1) Path-dependence of a strong kind occurs if and only if the propositional attitudes of an agent (individual or group) on a set of propositions violate strong consistency. Path-dependence of a weaker kind occurs if and only if these propositional attitudes are strongly consistent, but violate deductive closure. (2) If we impose universal domain, anonymity and completeness on a collective priority-to-the-past decision process, pathdependencies are unavoidable. (3) Path-dependence makes sequential decision processes vulnerable to manipulation by changes of the decision-path and to manipulation by expression of untruthful views on the propositions. I discuss three escape-routes from the problem of path-dependence: the special support, dictatorship and domain restriction approaches.

This course surveys a variety of reasoning, optimization, and decision-making methodologies for creating highly autonomous systems and decision support aids. The focus is on principles, algorithms, and their applications, taken from the disciplines of artificial intelligence and operations research. Reasoning paradigms include logic and deduction, heuristic and constraint-based search, model-based reasoning, planning and execution, reasoning under uncertainty, and machine learning. Optimization paradigms include linear, integer and dynamic programming. Decision-making paradigms include decision theoretic planning, and Markov decision processes. This course is offered both to undergraduate (16.410) students as a professional area undergraduate subject, in the field of aerospace information technology, and graduate (16.413) students.

In recent years, model checking has emerged as a remarkably effective technique for the automated analysis of descriptions of hardware systems and communication protocols. To analyze software system descriptions, however, a direct application of model checking rarely succeeds, since these descriptions often have huge (often infinite) state spaces that are not amenable to the finite-state methods of model checking. More important, the computation of a fixpoint (the hallmark of the model-checking approach) is not always needed in practice for the verification of an interesting class of properties, viz, properties that are invariantly true in all reachable states or transitions of the system. To establish a property as an invariant, an induction proof, suitably augmented with automatically generated lemmas, often suffices., Pub. in Formal Approaches to Agent-Based Systems, Jul 2001.

The classical algebraic modelling approach for integer programming (IP) is not suitable for some real world IP problems, since the algebraic formulations allow only for the description of mathematical relations, not logical relations. In this paper, we present a language L+ for IP, in which we write logical specification of an IP problem. L+ is a language based on the predicate logic, but is extended with meta predicates such as atJeast(m,S), where m is a non-negative integer, meaning that at least m predicates in the set 5 of formulas hold. The meta predicates facilitate reasoning about a model of an IP problem rigorously and logically. £+ is executable in the sense that formulas in £+ are mechanically translated into a set of mathematical formulas, called IP formulas, which most of existing IP solvers accept. We give a systematic method for translating formulas in £+ to IP formulas. The translation is rigorously defined, verified and implemented in Mathematica 3.0. Our work follows the approach of McKinnon and Williams, and elaborated the language in that (1) it is rigorously defined, (2) transformation to IP formulas is more optimised and verified, and (3) the transformation is completely given in Mathematica 3.0 and is integrated into IP solving environment as a tool for IP.

In this document we present symbolic algebraic modeling and analysis techniques applied to the landing gear subsystem in the new Swedish fighter aircraft, JAS 39 Gripen. This is a work in progress report within the larger project COmplex Hybrid SYstems (COHSY) which is a joint project between several academic (Mechanical Engineering, Computer Science and Electrical Engineering) and industrial (Saab Aircraft, Volvo Aero and VOAC) partners. It is also part of a long term effort within the Automatic Control group in Linköping to deal with discrete dynamic systems, mainly for control applications. Our methods are based on polynomials over finite fields (with Boolean algebra and propositional logic as special cases). Polynomials are used to represent the basic dynamic equations for the processes (controller and plant) as well as static properties of these. Temporal algebra (or temporal logic) is used to represent specifications of system behavior. We use this approach to model the landing gear controller from a partial documentation as well as the complete implementation in Pascal. We also provide temporal algebra interpretations of the specifications made available to us. Finally we perform a number of symbolic analyses (or verifications) on the complete process (controller and plant). The main results are: These methods and tools scale to problems of a non trivial size, i.e. of the size found in complex system designs such as the JAS 39. A first demonstration of possible uses of these methods and tools. Several interesting avenues of continued research motivated by problems found during this application.

In this document we present symbolic algebraic modeling and analysis techniques applied to the landing gear subsystem in the new Swedish fighter aircraft, JAS 39 Gripen. This is a work in progress report within the larger project COmplex Hybrid SYstems (COHSY) which is a joint project between several academic (Mechanical Engineering, Computer Science and Electrical Engineering) and industrial (Saab Aircraft, Volvo Aero and VOAC) partners. It is also part of a long term effort within the Automatic Control group in Linköping to deal with discrete dynamic systems, mainly for control applications. Our methods are based on polynomials over finite fields (with Boolean algebra and propositional logic as special cases). Polynomials are used to represent the basic dynamic equations for the processes (controller and plant) as well as static properties of these. Temporal algebra (or temporal logic) is used to represent specifications of system behavior. We use this approach to model the landing gear controller from a partial documentation as well as the complete implementation in Pascal. We also provide temporal algebra interpretations of the specifications made available to us. Finally we perform a number of symbolic analyses (or verifications) on the complete process (controller and plant). The main results are: These methods and tools scale to problems of a non trivial size, i.e. of the size found in complex system designs such as the JAS 39. A first demonstration of possible uses of these methods and tools. Several interesting avenues of continued research motivated by problems found during this application.

In a previous paper [Moore, 1983a, 1983b], we presented a nonmonotonic logic for modeling the beliefs of ideally rational agents who reflect on their own beliefs, which we called "autoepistemic logic." We defined a simple and intuitive semantics for autoepistemic logic and proved the logic sound and complete with respect to that semantics. However, the nonconstructive character of both the logic and its semantics made it difficult to prove the existence of sets of beliefs satisfying all the constraints of autoepistemic logic. This note presents an alternative, possible-world semantics for autoepistemic logic that enables us to construct finite models for autoepistemic theories, as well as to demonstrate the existence of sound and complete autoepistemic theories based on given sets of premises., To be presented at the Workshop on Nonmonotonic Reasoning held at the Mohonk Mountain House, New Paltz, NY on 17-19 October 1984.

Tato bakalářská práce se zabývá implementací systému pro automatické dokazování vět výrokové a predikátové logiky používajícím rezoluci. Cílem této práce je vytvořit jednoduchý systém a zdokumentovat jeho vývoj, nikoliv tvorba konkurenceschopného systému. Dále je v práci představeno několik populárních systémů automatického dokazování., This thesis focuses on implementation of resolution-based automatic theorem prover for propositional and first-order logic. The goal of this thesis is to create simple prover and document the development. Making state-of-the-art prover is not the goal of this thesis. We also present some popular automated theorem provers.

Tato bakalářská práce se zabývá implementací systému pro automatické dokazování vět výrokové a predikátové logiky používajícím rezoluci. Cílem této práce je vytvořit jednoduchý systém a zdokumentovat jeho vývoj, nikoliv tvorba konkurenceschopného systému. Dále je v práci představeno několik populárních systémů automatického dokazování., This thesis focuses on implementation of resolution-based automatic theorem prover for propositional and first-order logic. The goal of this thesis is to create simple prover and document the development. Making state-of-the-art prover is not the goal of this thesis. We also present some popular automated theorem provers.

Tato bakalářská práce se zabývá problematikou automatického dokazování ve výrokové a predikátové logice. V teoretické části je popsána výroková a predikátová logika v návaznosti na systém jejich automatického dokazování pomocí rezoluční metody. V práci je dále popsán návrh a implementace programu, který se skládá z terminálu a serverové části. Program hledá důkaz nesplnitelnosti zadané formule a vizualizuje jednotlivé kroky vedoucí k nalezení řešení. V závěru je vyhodnocena implementace řešení a práce jako celek a také jsou popsány další možnosti rozšíření., This bachelor’s thesis deals with problems in the area of automated reasoning in propositional and predicate logic. In the theoretical part the propositional and predicate logic is described in connection with the system of its automatic proving with help of resolution method. Further there is described draft and implementation of a program which consists of a terminal and server part. The program looks for a proof if the given formula is impossible to be solved and visualizes every single step which leads to finding of the solution. In conclusion the implementation of solution and the thesis as a whole is evaluated and there are also described additional possibilities of extension.

Tato práce popisuje algoritmy graphplan, satplan a real-time adaptive A*. Na implementaci těchto algoritmů je otestována jejich funkčnost a předpokládané vlastnosti (real-time výpočet, paralelismus), v netriviálních doménách. Graphplan a satplan jsou testovány v doménách block-world, tire-worl a bulldozer. Výsledky těchto algoritmů jsou porovnány a vykresleny do grafu. Real-time adaptive A* je testován v doméně tire-world. Dosažené výsledky jsou srovnány s klasickým A* a jsou zhodnoceny výhody a nevýhody těchto algoritmů., This work describes graphplan, satplan and real-time adaptive A* planning algorithms. Through implementation of these algorithms, functionality and assumed attributes (real-time calculation, parallelism) are tested. These tests take place in nontrivial domains. Graphplan and satplan algorithms were tested in block-world, tire-world and bulldozer domains. Results of these tests were compared and displayed in graphs. Real-time adaptive A* algorithm was tested in tire-world domain. Results of these tests were compared with classic A* algorithm. Advantages and disadvantages of these algorithms are also described in this work.

Tato bakalářská práce se zabývá implementací systému pro automatické dokazování vět výrokové a predikátové logiky používajícím rezoluci. Cílem této práce je vytvořit jednoduchý systém a zdokumentovat jeho vývoj, nikoliv tvorba konkurenceschopného systému. Dále je v práci představeno několik populárních systémů automatického dokazování., This thesis focuses on implementation of resolution-based automatic theorem prover for propositional and first-order logic. The goal of this thesis is to create simple prover and document the development. Making state-of-the-art prover is not the goal of this thesis. We also present some popular automated theorem provers.

Tato práce popisuje algoritmy graphplan, satplan a real-time adaptive A*. Na implementaci těchto algoritmů je otestována jejich funkčnost a předpokládané vlastnosti (real-time výpočet, paralelismus), v netriviálních doménách. Graphplan a satplan jsou testovány v doménách block-world, tire-worl a bulldozer. Výsledky těchto algoritmů jsou porovnány a vykresleny do grafu. Real-time adaptive A* je testován v doméně tire-world. Dosažené výsledky jsou srovnány s klasickým A* a jsou zhodnoceny výhody a nevýhody těchto algoritmů., This work describes graphplan, satplan and real-time adaptive A* planning algorithms. Through implementation of these algorithms, functionality and assumed attributes (real-time calculation, parallelism) are tested. These tests take place in nontrivial domains. Graphplan and satplan algorithms were tested in block-world, tire-world and bulldozer domains. Results of these tests were compared and displayed in graphs. Real-time adaptive A* algorithm was tested in tire-world domain. Results of these tests were compared with classic A* algorithm. Advantages and disadvantages of these algorithms are also described in this work.

Tato práce popisuje algoritmy graphplan, satplan a real-time adaptive A*. Na implementaci těchto algoritmů je otestována jejich funkčnost a předpokládané vlastnosti (real-time výpočet, paralelismus), v netriviálních doménách. Graphplan a satplan jsou testovány v doménách block-world, tire-worl a bulldozer. Výsledky těchto algoritmů jsou porovnány a vykresleny do grafu. Real-time adaptive A* je testován v doméně tire-world. Dosažené výsledky jsou srovnány s klasickým A* a jsou zhodnoceny výhody a nevýhody těchto algoritmů., This work describes graphplan, satplan and real-time adaptive A* planning algorithms. Through implementation of these algorithms, functionality and assumed attributes (real-time calculation, parallelism) are tested. These tests take place in nontrivial domains. Graphplan and satplan algorithms were tested in block-world, tire-world and bulldozer domains. Results of these tests were compared and displayed in graphs. Real-time adaptive A* algorithm was tested in tire-world domain. Results of these tests were compared with classic A* algorithm. Advantages and disadvantages of these algorithms are also described in this work.