Skip to content

Commit

Permalink
Fix bug in classical tableaux biconditional negation rule
Browse files Browse the repository at this point in the history
  • Loading branch information
ariroffe committed Mar 23, 2024
1 parent 9acad2c commit 1fa03a7
Show file tree
Hide file tree
Showing 4 changed files with 14 additions and 10 deletions.
4 changes: 4 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,10 @@ All notable changes to this project will be documented in this file.
The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).

## [1.10.1] - 2024-03-23
### Fixed
- Bug in the biconditional rule of classical tableaux system

## [1.10.0] - 2024-02-29
### Added
- Model finder for classical model theory w/documentation and tests
Expand Down
2 changes: 1 addition & 1 deletion docs/source/conf.py
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@
author = 'Ariel Jonathan Roffe'

# The full version, including alpha/beta/rc tags
release = '1.10.0'
release = '1.10.1'


# -- General configuration ---------------------------------------------------
Expand Down
16 changes: 8 additions & 8 deletions logics/instances/propositional/tableaux.py
Original file line number Diff line number Diff line change
Expand Up @@ -84,16 +84,16 @@
'''

classical_neg_biconditional_rule = TableauxNode(content=Formula(['~', ['↔', ['A'], ['B']]]))
cnbr2 = TableauxNode(content=Formula(['~', ['A']]), justification='R↔', parent=classical_neg_biconditional_rule)
TableauxNode(content=Formula(['B']), justification='R↔', parent=cnbr2)
cnbr3 = TableauxNode(content=Formula(['A']), justification='R↔', parent=classical_neg_biconditional_rule)
TableauxNode(content=Formula(['~', ['B']]), justification='R↔', parent=cnbr3)
cnbr2 = TableauxNode(content=Formula(['~', ['A']]), justification='R~↔', parent=classical_neg_biconditional_rule)
TableauxNode(content=Formula(['B']), justification='R~↔', parent=cnbr2)
cnbr3 = TableauxNode(content=Formula(['A']), justification='R~↔', parent=classical_neg_biconditional_rule)
TableauxNode(content=Formula(['~', ['B']]), justification='R~↔', parent=cnbr3)
'''
['~', ['↔', ['A'], ['B']]]
├── ['~', ['A']] (R↔)
│ └── ['B'] (R↔)
└── ['A'] (R↔)
└── ['~', ['B']] (R↔)
├── ['~', ['A']] (R~↔)
│ └── ['B'] (R~↔)
└── ['A'] (R~↔)
└── ['~', ['B']] (R~↔)
'''

classical_tableaux_rules = {
Expand Down
2 changes: 1 addition & 1 deletion setup.cfg
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[metadata]
name = logics
version = 1.10.0
version = 1.10.1
author = Ariel Jonathan Roffé
author_email = arielroffe@filo.uba.ar
url = https://github.com/ariroffe/logics
Expand Down

0 comments on commit 1fa03a7

Please sign in to comment.