Search Results - "modal logic"

A Concise Introduction to Logic by DeLancey, Craig

Access online version

VIRTUAL UNIVERSITY: EDUCATION AS A LIFESTYLE by Denys Svyrydenko, Valentyna Kyvliuk

Connect to this object online.

Epistemic Game Theory and Logic by Paul Weirich (Ed.)

DOAB: download the publication
DOAB: description of the publication

The Many and the One A Philosophical Study of Plural Logic by Florio, Salvatore

DOAB: download the publication
DOAB: description of the publication

Automated Reasoning with Analytic Tableaux and Related Methods 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings /

Table of Contents: “…Range-Restricted and Horn Interpolation through Clausal Tableaux -- Non-Classical Logics in Satisfiability Modulo Theories -- DefTab: A Tableaux System for Sceptical Consequence in Default Modal Logics -- Non-distributive description logic -- A new calculus for intuitionistic Strong L\"ob logic: strong termination and cut-elimination, formalized -- Some Analytic Systems of Rules -- A cut-free, sound and complete Russellian theory of definite descriptions -- Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators -- Lemmas: Generation, Selection, Application -- Machine-Learned Premise Selection for Lean -- gym-saturation: Gymnasium environments for saturation provers (System description) -- A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points -- Ill-founded Proof Systems For Intuitionistic Linear-time Temporal Logic -- Proof Systems for the Modal $\mu$-Calculus Obtained by Determinizing Automata -- Extensions of K5: Proof Theory and Uniform Lyndon Interpolation -- On intuitionistic diamonds (and lack thereof) -- NP Complexity for Combinations of Non-Normal Modal Logics -- Resolution-based Calculi for Non-Normal Modal Logics -- Canonicity of Proofs in Constructive Modal Logic -- Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic -- The MaxSAT problem in the real-valued MV-algebra -- The Logic of Separation Logic: Models and Proofs -- Testing the Satisfiability of Formulas in Separation Logic with Permissions -- Nested Sequents for Quantified Modal Logics -- A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness.…”
Link to Metadata

The Many and the One A Philosophical Study of Plural Logic by Florio, Salvatore

OAPEN Library: download the publication
OAPEN Library: description of the publication

Automated Deduction - CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings /

Table of Contents: “…Certified Core-Guided MaxSAT Solving -- Superposition with Delayed Unification -- On Incremental Pre-processing for SMT -- Verified Given Clause Procedures -- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment -- Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs -- An Isabelle/HOL Formalization of the SCL(FOL) Calculus -- SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning -- Formal Reasoning about Influence in Natural Sciences Experiments -- A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification) -- SAT-Based Subsumption Resolution -- A more Pragmatic CDCL for IsaSAT and targetting LLVM (Short Paper) -- Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper) -- COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description) -- Choose your Colour: Tree Interpolation for Quantified Formulas in SMT -- Proving Termination of C Programs with Lists -- Reasoning about Regular Properties: A Comparative Study -- Program Synthesis in Saturation -- A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus -- Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs -- Verification of NP-hardness Reduction Functions for Exact Lattice Problems -- Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic -- Left-Linear Completion with AC Axioms -- On P -interpolation in local theory extensions and applications to the study of interpolation in the description logics EL, EL+ -- Theorem Proving in Dependently-Typed Higher-Order Logic -- Towards Fast Nominal Anti-Unification of Letrec-Expressions -- Confluence Criteria for Logically Constrained Rewrite Systems -- Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory -- An Experimental Pipeline for Automated Reasoning in Natural Language (Short paper) -- Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness -- Decidability of difference logic over the reals with uninterpreted unary predicates -- Incremental Rewriting Modulo SMT -- Iscalc: an Interactive Symbolic Computation Framework (System Description).…”
Link to Metadata

Open Logic Project by Zach, Richard, Arana, Andrew, Avigad, Jeremy, Dean, Walter, Russell, Gillian, Wyatt, Nicole, Yap, Audrey

Table of Contents: “…I Naıve Set Theory -- II Propositional Logic -- III First-order Logic -- IV Model Theory -- V Computability -- VI Turing Machines -- VII Incompleteness -- VIII Second-order Logic -- IX The Lambda Calculus -- X Many-valued Logic -- XI Normal Modal Logics -- XII Intuitionistic Logic -- XIII Counterfactuals -- XIV Set Theory -- XV Methods -- XVI History…”
Access online version

Automated Deduction - CADE 28 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings /

Table of Contents: “…Invited Talks -- Non-well-founded Deduction for Induction and Coinduction -- Towards the Automatic Mathematician -- Logical Foundations -- Tableau-based decision procedure for non-Fregean logic of sentential identity -- Learning from Lukasiewicz and Meredith: Investigations into Proof Structures -- Efficient Local Reductions to Basic Modal Logic -- Isabelle's Metalogic: Formalization and Proof Checker -- Theory and Principles -- The ksmt calculus is a delta-complete decision procedure for non-linear constraints -- Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning -- Politeness and Stable Infiniteness: Stronger Together -- Equational Theorem Proving Modulo -- Unifying Decidable Entailments in Separation Logic with Inductive Definitions -- Subformula Linking for Intuitionistic Logic with Application to Type Theory -- Efficient SAT-based Proof Search in Intuitionistic Propositional Logic -- Proof Search and Certificates for Evidential Transactions -- Non-Clausal Redundancy Properties -- Multi-Dimensional Interpretation Methods for Termination of Term Rewriting -- Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures -- Computing Optimal Repairs of Quantified ABoxes w.r.t. …”
Link to Metadata

Automated Reasoning 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings

DOAB: download the publication
DOAB: description of the publication

Automated Reasoning 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings

OAPEN Library: download the publication
OAPEN Library: description of the publication