Automated Reasoning
8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016, Proceedings
Page
%P
-
Chapter and Conference Paper
Local Intuitionistic Modal Logics and Their Calculi
We investigate intuitionistic modal logics with locally interpreted \(\square \) □ ...
-
Chapter and Conference Paper
Resolution Calculi for Non-normal Modal Logics
We present resolution calculi for the cube of classical non-normal modal logics. The calculi are based on a simple clausal form that comprises both local and global clauses. Any formula can be efficiently tran...
-
Chapter and Conference Paper
Dyadic Obligations: Proofs and Countermodels via Hypersequents
The basic system \(\textbf{E}\) E of dyadic deontic logic p...
-
Chapter and Conference Paper
Labelled Sequent Calculi for Conditional Logics: Conditional Excluded Middle and Conditional Modus Ponens Finally Together
We introduce labelled sequent calculi for Conditional Logics with a selection function semantics. Conditional Logics are a sort of generalization of multimodal logics where modalities are labelled by formulas ...
-
Chapter and Conference Paper
Towards an Intuitionistic Deontic Logic Tolerating Conflicting Obligations
We propose a minimal deontic logic, called MIND, based on intuitionistic logic. This logic gives a very simple solution to handling conflicting obligations: the presence of two conflicting obligations does not...
-
Chapter and Conference Paper
Terminating Calculi and Countermodels for Constructive Modal Logics
We investigate terminating sequent calculi for constructive modal logics \(\mathsf {CK}\) CK ...
-
Article
Intuitionistic Non-normal Modal Logics: A General Framework
We define a family of intuitionistic non-normal modal logics; they can be seen as intuitionistic counterparts of classical ones. We first consider monomodal logics, which contain only Necessity or Possibility....
-
Chapter and Conference Paper
HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)
We present HYPNO (HYpersequent Prover for NOn-normal modal logics), a Prolog-based theorem prover and countermodel generator for non-normal modal logics. HYPNO implements some hypersequent calculi recently introd...
-
Chapter
Automated Deduction
After a brief history and motivation of Automated Deduction (AD), the notions of order logic are defined and aspects of the Superposition calculus and semantic tableaux are presented. This last can be ...
-
Chapter and Conference Paper
Countermodel Construction via Optimal Hypersequent Calculi for Non-normal Modal Logics
We develop semantically-oriented calculi for the cube of non-normal modal logics and some deontic extensions. The calculi manipulate hypersequents and have a simple semantic interpretation. Their main feature ...
-
Chapter and Conference Paper
Nested Sequents for the Logic of Conditional Belief
The logic of conditional belief, called Conditional Doxastic Logic ( \(\mathsf {CDL}\) ), was proposed by Boa...
-
Chapter and Conference Paper
PRONOM: Proof-Search and Countermodel Generation for Non-normal Modal Logics
We present PRONOM, a theorem prover and countermodel generator for non-normal modal logics. PRONOM implements some labelled sequent calculi recently introduced for the basic system \(\mathbf {E}\) and its extensi...
-
Chapter and Conference Paper
VINTE: An Implementation of Internal Calculi for Lewis’ Logics of Counterfactual Reasoning
We present VINTE, a theorem prover for conditional logics for counterfactual reasoning introduced by Lewis in the seventies. VINTE implements some internal calculi recently introduced for the basic system ...
-
Chapter and Conference Paper
Hypersequent Calculi for Lewis’ Conditional Logics with Uniformity and Reflexivity
We present the first internal calculi for Lewis’ conditional logics characterized by uniformity and reflexivity, including non-standard internal hypersequent calculi for a number of extensions of the logic ...
-
Book and Conference Proceedings
-
Chapter and Conference Paper
Standard Sequent Calculi for Lewis’ Logics of Counterfactuals
We present new sequent calculi for Lewis’ logics of counterfactuals. The calculi are based on Lewis’ connective of comparative plausibility and modularly capture almost all logics of Lewis’ family. Our calculi...
-
Chapter and Conference Paper
A Sequent Calculus for Preferential Conditional Logic Based on Neighbourhood Semantics
The basic preferential conditional logic PCL, initially proposed by Burgess, finds an interest in the formalisation of both counterfactual and plausible reasoning, since it is at the same time more general tha...
-
Chapter and Conference Paper
A Multi-engine Theorem Prover for a Description Logic of Typicality
We describe DysToPic, a theorem prover for the preferential Description Logic \(\mathcal {ALC}+\mathbf{T}_{min}\) .Thi...
-
Chapter and Conference Paper
A Standard Internal Calculus for Lewis’ Counterfactual Logics
The logic \({\mathbb V}\) is the basic logic of counterfactuals in the family of Lewis’ systems. It is charac...
-
Chapter and Conference Paper
NESCOND: An Implementation of Nested Sequent Calculi for Conditional Logics
We present NESCOND, a theorem prover for normal conditional logics. NESCOND implements some recently introduced NESted sequent calculi for propositional CONDitional logics CK and some of its significant extens...
