Logic for programming, artificial intelligence, and reasoning

Más información sobre el libro

The book covers a range of topics in logic and computational theory, beginning with an exploration of Hilbert’s Program and its evolution into a logic toolbox. It discusses vacuous truth and the challenges in deductive question answering, alongside decidable fragments of many-sorted logic. The text delves into one-pass tableaux for computation tree logic and extends resolution provers to handle inequalities on elementary functions. It also examines model checking within the first-order fragment of higher-order fixpoint logic and the decidability of monadic fragments of Gödel logics. Key concepts include fixed points in linear logic, semantics of consistency and trust in peer data exchange, and completeness in sequence logic. The book introduces Zenon, an extensible automated theorem prover, and addresses matching in hybrid terminologies. It covers the verification of cryptographic protocols and knowledge in security protocols, as well as mechanized verification of CPS transformations. Further discussions include operational and epistemic approaches to protocol analysis, verification methods, and extensions of abstract categorial grammars. The content also touches on finite satisfiability in the guarded fragment, data complexity in description logics, and algorithms for propositional model counting. Lastly, it addresses the complexity of temporal logic and ATP cross-verification of Mizar MPTP challenge problems.