We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKπ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory.

We study straightforward embeddings of propositional normal multimodal logic and propositional intuitionistic logic in simple type theory. The correctness of these embeddings is easily shown. We give examples to demonstrate that these embeddings provide an effective framework for computational investigations of various non-classical logics. We report some experiments using the higher-order automated theorem prover LEO-II.

Logic and Computation is concerned with techniques for formal theorem-proving, with particular reference to Cambridge LCF (Logic for Computable Functions). Cambridge LCF is a computer program for reasoning about computation. It combines methods of mathematical logic with domain theory, the basis of the denotational approach to specifying the meaning of statements in a programming language. This book consists of two parts. Part I outlines the mathematical preliminaries: elementary logic and domain theory. They are explained at an intuitive level, giving references (...) to more advanced reading. Part II provides enough detail to serve as a reference manual for Cambridge LCF. It will also be a useful guide for implementors of other programs based on the LCF approach. (shrink)

Ackermann’s function can be expressed using an iterative algorithm, which essentially takes the form of a term rewriting system. Although the termination of this algorithm is far from obvious, its equivalence to the traditional recursive formulation—and therefore its totality—has a simple proof in Isabelle/HOL. This is a small example of formalising mathematics using a proof assistant, with a focus on the treatment of difficult recursions.

The Routledge Handbook of Collective Intelligence for Democracy and Governance explores the concepts, methodologies, and implications of collective intelligence for democratic governance, in the first comprehensive survey of this field. Illustrated by a collection of inspiring case studies and edited by three pioneers in collective intelligence, this handbook serves as a unique primer on the science of collective intelligence applied to public challenges and will inspire public actors, academics, students, and activists across the world to apply collective intelligence in policymaking (...) and administration to explore its potential, both to foster policy innovations and reinvent democracy. The Routledge Handbook of Collective Intelligence for Democracy and Governance is essential reading and an authoritative reference for scholars, students, researchers and practitioners of public policy, public administration, governance, public management, information technology and systems, innovation and democracy as well as more broadly for political science, psychology, management studies, public organizations and individual policy practitioners, public authorities, civil society activists and service providers. (shrink)

This book tells an overlooked story in the history of the will, a contested idea in both politics and philosophy of mind. For it is Cicero, statesman and philosopher, who gives shape to the notion of will as it would become in Western thought and who invents the idea of 'the will of the people'. In a single word – voluntas – he brings Roman law in contact with Greek ideas, chief among them Plato's claim that a rational elite must (...) rule. When the republic falls to Caesarism, Cicero turns his political argument inward: will is a force to win the virtue in the soul that was lost on the battlefield, the marker of inner freedom in an unfree age. Though his vision of a free republic failed in his time, Cicero's ideal of rational elitism has shaped and fractured the modern world – and Ciceronian creativity may yet save it. (shrink)