Theorem proving for conditional logics: CondLean and GOALDUCK
From MaRDI portal
Publication:3643366
DOI10.3166/JANCL.18.427-473zbMATH Open1180.03014OpenAlexW2075938707MaRDI QIDQ3643366FDOQ3643366
Authors: N. Olivetti, G. L. Pozzato 
Publication date: 11 November 2009
Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.3166/jancl.18.427-473
Recommendations
- CondLean: a theorem prover for conditional logics
- A sequent calculus and a theorem prover for standard conditional logics
- scientific article; zbMATH DE number 1696800
- Some Completeness Results for Propositional Conditional Logics
- Proof by consistency in conditional equational theories
- From input/output logics to conditional logics via sequents -- with provers
- On goal-directed provability in classical logic
- A family of goal directed theorem provers based on conjunction and implication. I
- Theorem proving for prenex Gödel logic with \(\Delta\): checking validity and unsatisfiability
- Computer Science Logic
sequent calculitheorem provingconditional logicsgoal-directed proof methodslabeled deductive systems
Cites Work
- lean\(T^ AP\): Lean tableau-based deduction
- Nonmonotonic reasoning, preferential models and cumulative logics
- Plausibility measures and default reasoning
- Goal-directed proof theory
- Basic conditional logic
- A Gentzen- or Beth-type system, a practical decision procedure and a constructive completeness proof for the counterfactual logics VC and VCS
- Labelled Tableaux for Nonmonotonic Reasoning: Cumulative Consequence Relations
- Title not available (Why is that?)
- Uniform proofs as a foundation for logic programming
- Updates and counterfactuals
- Conditional reasoning in logic programming
- A first-order conditional logic for prototypical properties
- Conditional logic of actions and causation
- A general approach for determining the validity of commonsense assertions using conditional logics
- Iterated belief revision and conditional logic
- A sequent- or tableau-style system for Lewis's counterfactual logic VC
- Tableaux for nonmonotonic logics
- lean TAP revisited
- Automated reasoning with analytic tableaux and related methods. 16th international conference, TABLEAUX 2007, Aix en Provence, France, July 3--6, 2007. Proceedings.
- Weak AGM postulates and strong Ramsey test: A logical formalization
Cited In (7)
- KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning
- Embedding and automating conditional logics in classical higher-order logic
- CSL-lean: A Theorem-prover for the Logic of Comparative Concept Similarity
- A general approach for determining the validity of commonsense assertions using conditional logics
- CondLean: a theorem prover for conditional logics
- Mechanising Gödel-Löb provability logic in HOL light
- Automated Reasoning with Analytic Tableaux and Related Methods
Uses Software
This page was built for publication: Theorem proving for conditional logics: CondLean and GOALDUCK
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3643366)
