judge 0.1.2.0 → 0.1.3.0
raw patch · 13 files changed
+205/−152 lines, 13 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- CHANGELOG.md +10/−0
- README.md +14/−10
- app/Main.hs +0/−6
- formulas.txt +9/−6
- judge.cabal +6/−5
- logic/J-ghari.yml +0/−81
- logic/J.yml +0/−38
- logic/J0-PB.yml +86/−0
- logic/J0.yml +38/−0
- logic/LP.yml +3/−2
- logic/example.yml +38/−0
- src/Logic/Judge/Formula/Datastructure.hs +0/−3
- src/Logic/Judge/Prover/Tableau.hs +1/−1
CHANGELOG.md view
@@ -10,6 +10,16 @@ Unreleased ---------- +[0.1.3.0] - 2018-03-14+----------------------++### Changed++ * Changed name and description of data files.+ * Fixed bug that caused assumptions not to be simplified.+++ [0.1.2.0] - 2018-01-19 ----------------------
README.md view
@@ -9,16 +9,20 @@ Installation ------------------------------------------------------------------------------ -After cloning the repository, the recommended installation method is through -[Stack](https://www.stackage.org/):+`judge` can be installed through +[Cabal](https://www.haskell.org/cabal/users-guide/): - stack install judge+ cabal sandbox init+ cabal install judge -Alternatively, `judge` can be installed through -[Cabal](https://www.haskell.org/cabal/users-guide/). +A recommended alternative is to use [Stack](https://www.stackage.org/), for +which you will need to clone the repository and do: + stack install ++ Usage ------------------------------------------------------------------------------- @@ -26,7 +30,8 @@ or [JSON](http://json.org/) format. This file will specify the type of proof system and the logical family (although at the moment, only the respective values `tableau` and `justification` are recognised). It also provides the -rules of inference. See the [logic](logic) directory for examples.+rules of inference. See the [logic](logic) directory for example +specifications. If no target formula(s) are provided via `-g`, formulas are read off the standard input. If no output file is provided via `-o`, the result is written @@ -34,10 +39,10 @@ to obtain LaTeX code instead. For example, the following will construct proofs for [theorems](formulas.txt) -of the logic [Jcs](logic/J.yml) (with `c:(A→B→A) ∊ CS`), and produces a PDF +of the logic [LP](logic/LP.yml) (with `c:(A→B→A) ∊ CS`), and produces a PDF file to visualise them: - judge logic/J.yml \+ judge LP \ -a "c:(A->B->A)" \ -f LaTeX \ < formulas.txt \@@ -49,8 +54,7 @@ ------------------------------------------------------------------------------- Notable missing features are detailed on the [issue -tracker](https://github.com/slakkenhuis/judge/issues) -([export](https://api.github.com/repos/slakkenhuis/judge/issues)).+tracker](https://github.com/slakkenhuis/judge/issues). Contributions that extend `judge` to different logical families (modal, first order...) or proof systems (sequent, natural deduction...) are welcomed.
app/Main.hs view
@@ -46,12 +46,6 @@ <$> (deserialise yaml :: IO (T.TableauSystem F.Justification)) <*> (CLI.assumptions arg :: IO [F.FormulaJL]) - -- Tableau system is not prettyprinted well, so won't be shown- -- even in verbose mode for now- --if CLI.verbose arg- -- then write stderr $ pretty sys- -- else return ()- targets <- CLI.goals arg :: IO [F.FormulaJL] file <- CLI.outfile arg let format = CLI.format arg
formulas.txt view
@@ -3,18 +3,21 @@ ############################################################################## # A simple propositional test-(~r → p) & (r → q) -> (p | q)+(~r -> p) & (r -> q) -> (p | q) -# The Application axiom should derive instantly in both j0-new and j0-ghari-x:A → y:(A → B) -> y*x:B+# The Application axiom should derive instantly in both J0 and J0-PB+x:A → y:(A → B) → y*x:B # ... and this one should fail instantly-x:A → y:(A → B) -> x*y:B+x:A → y:(A → B) → x*y:B -# This is a good one: it works in both j0-new and j0-ghari, but inspects about +# Using proof checker, should work only in LP+x:a → y:(x:a → b) → y·!x:b++# This is a good one: it works in both J0 and J0-PB, but inspects about # 18000 formulas in the latter (or 8000 if x:A is in the CS instead of the # antecedent) x:A → y:(A → B) → y*(x+x'):B -# ... And this one just gets too complex to find at all+# ... and this one just gets too complex to find at all x:A → y:(A → B) → (y+y')*x:B
judge.cabal view
@@ -1,8 +1,8 @@ name: judge-version: 0.1.2.0-synopsis: Tableau-based theorem prover.+version: 0.1.3.0+synopsis: Tableau-based theorem prover for justification logic. description: An implementation of a decision procedure for classical - logic and justification logic.+ propositional logic and justification logic. homepage: https://github.com/slakkenhuis/judge#readme license: GPL-3 license-file: LICENSE@@ -13,9 +13,10 @@ extra-source-files: README.md , CHANGELOG.md , formulas.txt-data-files: logic/J.yml+data-files: logic/J0.yml , logic/LP.yml- , logic/J-ghari.yml+ , logic/J0-PB.yml+ , logic/example.yml cabal-version: >=1.10 library
− logic/J-ghari.yml
@@ -1,81 +0,0 @@-logic: justification-system: tableau-name: J₀-description: |- This system stays mostly faithful to the one described in Ghari 2016. The - CSr rule was not present in the original; it emulates closure upon- encountering [F] φ on the branch for some φ ∊ CS.-rules:- - name: "Te"- consume: ["[T] T:A"]- produce:- - ["[T, e] T:A"]-- - name: "Fe"- consume: ["[F] T:A"]- produce:- - ["[F, e] T:A"]-- - name: "F→"- consume: ["[F] A → B"]- produce: - - ["[T] A", "[F] B"]-- - name: "T→"- consume: ["[T] A -> B"]- produce:- - ["[F] A"]- - ["[T] B"]-- - name: "F+"- consume: ["[F, e] T+S:A"]- produce:- - ["[F, e] T:A", "[F, e] S:A"]-- - name: "T·"- consume: ["[T, e] S:(A → B)", "[T, e] T:A"]- produce:- - ["[T, e] (S * T) : B"]- restrict:- and:- - match: "A → B"- with: [subterms, formulas]- in:- union: [root, assumptions]- - match: "S * T"- with: subterms- in: root- - name: "CSr"- consume: []- produce:- - ["[T] A"]- generate:- match: "A"- with: all- in: assumptions- - name: "PBe"- consume: []- produce:- - ["[T, e] T:A"]- - ["[F, e] T:A"]- generate:- and:- - match: "A"- with: [subterms, formulas]- in: - union: [root, assumptions]- - match: "T"- with: [subterms, justifications]- in: root-- - name: "PBf"- consume: []- produce:- - ["[T] A"]- - ["[F] A"]- generate:- match: "A"- with: [subterms, formulas]- in: - union: [root, assumptions]-
− logic/J.yml
@@ -1,38 +0,0 @@-logic: justification-system: tableau-name: J₀-description: |- This is the system described in my thesis.-rules:- - name: "F→"- consume: ["[F] A → B"]- produce: - - ["[T] A", "[F] B"]- - name: "F+"- consume: ["[F] T+S:A"]- produce: - - ["[F] T:A", "[F] S:A"]- - name: "T→"- consume: ["[T] A -> B"]- produce:- - ["[F] A"]- - ["[T] B"]- - name: "F·"- consume: ["[F] (S * T) : B"]- produce:- - ["[F] S:(A → B)"]- - ["[F] T:A"]- generate:- match: "A → B"- with: [subterms, formulas]- in:- union: [root, assumptions]- - name: "CSr"- consume: []- produce:- - ["[T] A"]- generate:- match: "A"- with: all- in: assumptions-assumptions: []
+ logic/J0-PB.yml view
@@ -0,0 +1,86 @@+logic: justification+system: tableau+name: J₀+description: |+ This is a system for the justification logic J0 (and Jcs, when formulas + from the constant specification are added.+ + It is decidable through the addition of the principle of bivalence, as + suggested by Finger (2010) and Ghari (2016). This particular system is + based on the one described by Ghari, although the rule CSr was not+ present in the original; it emulates closure of the branch upon + encountering [F] φ for some φ ∊ CS.+rules:+ - name: "Te"+ consume: ["[T] T:A"]+ produce:+ - ["[T, e] T:A"]++ - name: "Fe"+ consume: ["[F] T:A"]+ produce:+ - ["[F, e] T:A"]++ - name: "F→"+ consume: ["[F] A → B"]+ produce: + - ["[T] A", "[F] B"]++ - name: "T→"+ consume: ["[T] A -> B"]+ produce:+ - ["[F] A"]+ - ["[T] B"]++ - name: "F+"+ consume: ["[F, e] T+S:A"]+ produce:+ - ["[F, e] T:A", "[F, e] S:A"]++ - name: "T·"+ consume: ["[T, e] S:(A → B)", "[T, e] T:A"]+ produce:+ - ["[T, e] (S * T) : B"]+ restrict:+ and:+ - match: "A → B"+ with: [subterms, formulas]+ in:+ union: [root, assumptions]+ - match: "S · T"+ with: subterms+ in: root+ - name: "CSr"+ consume: []+ produce:+ - ["[T] A"]+ generate:+ match: "A"+ with: all+ in: assumptions+ - name: "PBe"+ consume: []+ produce:+ - ["[T, e] T:A"]+ - ["[F, e] T:A"]+ generate:+ and:+ - match: "A"+ with: [subterms, formulas]+ in: + union: [root, assumptions]+ - match: "T"+ with: [subterms, justifications]+ in: root++ - name: "PBf"+ consume: []+ produce:+ - ["[T] A"]+ - ["[F] A"]+ generate:+ match: "A"+ with: [subterms, formulas]+ in: + union: [root, assumptions]+
+ logic/J0.yml view
@@ -0,0 +1,38 @@+logic: justification+system: tableau+name: J₀+description: |+ This is the system for J₀ (and Jcs, if the constant specification is + added) described in my Master's thesis.+rules:+ - name: "F→"+ consume: ["[F] φ → ψ"]+ produce: + - ["[T] φ", "[F] ψ"]+ - name: "F+"+ consume: ["[F] T+S:φ"]+ produce: + - ["[F] T:φ", "[F] S:φ"]+ - name: "T→"+ consume: ["[T] φ → ψ"]+ produce:+ - ["[F] φ"]+ - ["[T] ψ"]+ - name: "F·"+ consume: ["[F] (S · T) : ψ"]+ produce:+ - ["[F] S:(φ → ψ)"]+ - ["[F] T:φ"]+ generate:+ match: "φ → ψ"+ with: [subterms, formulas]+ in:+ union: [root, assumptions]+ - name: "CSr"+ consume: []+ produce:+ - ["[T] φ"]+ generate:+ match: "φ"+ with: all+ in: assumptions
logic/LP.yml view
@@ -2,7 +2,8 @@ system: tableau name: Logic of proofs description: |- This is the system for LP described in my thesis.+ This is the system for LP (and LPcs, if the constant specification is + added) described in my Master's thesis. rules: - name: "F→" consume: ["[F] A → B"]@@ -21,7 +22,7 @@ produce: - ["[F] T:A"] - name: "T→"- consume: ["[T] A -> B"]+ consume: ["[T] A → B"] produce: - ["[F] A"] - ["[T] B"]
+ logic/example.yml view
@@ -0,0 +1,38 @@+logic: "justification"+system: "tableau"+rules:+ - name: "F→"+ consume: ["[F] φ → ψ"]+ produce: + - - "[T] φ"+ - "[F] ψ"+ - name: "T→"+ consume: ["[T] φ → ψ"]+ produce:+ - - "[F] φ"+ - - "[T] ψ"+ - name: "T·"+ consume: ["[T] S:(φ → ψ)", "[T] T:φ"]+ produce:+ - - "[T] S·T:ψ"+ restrict:+ and:+ - match: "φ → ψ"+ with: ["subterms", "formulas"]+ in:+ union: ["root", "assumptions"]+ - match: "S · T"+ with: "subterms"+ in: "root"+ - name: "CSr"+ consume: []+ produce:+ - - "[T] φ"+ generate:+ match: "φ"+ with: "all"+ in: "assumptions"+ compose: "greedy"+assumptions:+ - "c:(A→(B→A))"+
src/Logic/Judge/Formula/Datastructure.hs view
@@ -116,9 +116,6 @@ instance Functor Marked where fmap f (Marked marks x) = Marked marks (f x) ---mark :: [String] -> Marked a -> Marked a---mark new (Marked old x) = Marked (new ++ old) x- -- BASIC MANIPULATIONS -------------------------------------------------------
src/Logic/Judge/Prover/Tableau.hs view
@@ -360,7 +360,7 @@ initκ = TableauSettings { rulesC = rulesC , root = value $ L.current root- , assumptions = assumptions' system+ , assumptions = map F.simplify $ assumptions' system } -- | Initial branch