Popularity
4.8
Growing
Activity
0.0
Stable
4
3
2

Tags: Logic     Theorem Provers

# structural-induction alternatives and similar packages

Based on the "Logic" category.
Alternatively, view structural-induction alternatives based on common mentions on social networks and blogs.

• ### tamarin-prover

Main source code repository of the Tamarin prover for security protocol verification.
• ### hatt

Truth-table generator for classical propositional logic

• ### smcdel

A symbolic model checker for Dynamic Epistemic Logic.

Haskell version of the code from "Handbook of Practical Logic and Automated Reasoning"

• ### picologic

Symbolic logic expressions
• ### jukebox

A theorem prover

• ### logic-classes

Framework for propositional and first order logic, theorem proving
• ### hout

A non-interactive proof assistant using the Haskell type system
• ### obdd

pure Haskell implementation of reduced ordered binary decision diagrams

• ### g4ip-prover

Theorem prover for intuitionistic propositional logic, fork of github.com/cacay/G4ip

SAT encoder
• ### qed

Experiments writing a prover
• ### tpdb

parser and prettyprinter for TPDB syntax (termination problem data base)
• ### g4ip

A theorem prover using G4ip

• ### judge

Tableau-based theorem prover for justification logic.

The core logical system of the HaskHOL theorem prover. See haskhol.org for more details.

Do you think we are missing an alternative of structural-induction or a related project?

### Popular Comparisons

This package aims to perform the fiddly details of instantiating induction schemas for algebraic data types. The library is parameterised over the type of variables (`v`), constructors (`c`) and types (`t`).

Let's see how it looks if you instantiate all these three with String and want to do induction over natural numbers. First, one needs to create a type environment, a `TyEnv`. For every type (we only have one), we need to list its constructors. For each constructor, we need to list its arguments and whether they are recursive or not.

``````testEnv :: TyEnv String String
testEnv "Nat" = Just [ ("zero",[]) , ("succ",[Rec "Nat"]) ]
testEnv _ = Nothing
``````

Now, we can use the `subtermInduction` to get induction hypotheses which are just subterms of the conclusion. Normally, you would translate the `Term`s from the proof `Obligation`s to some other representation, but there is also linearisation functions included (`linObligations`, for instance.)

``````natInd :: [String] -> [Int] -> IO ()
natInd vars coords = putStrLn
\$ render
\$ linObligations strStyle
\$ unTag (\(x :~ i) -> x ++ show i)
\$ subtermInduction testEnv typed_vars coords
where
typed_vars = zip vars (repeat "Nat")
``````

The library will create fresh variables for you (called `Tagged` variables), but you need to remove them, using for instance `unTag`. If you want to sync it with your own name supply, use `unTagM` or `unTagMapM`.

An example invocation:

``````*Mini> natInd ["X"] 
P(zero).
! [X1 : Nat] : (P(X1) => P(succ(X1))).
``````

This means to do induction on the zeroth coord (hence the `0`), and the variable is called "X". When using the library, it is up to you to translate the abstract `P` predicate to something meaningful.

We can also do induction on several variables:

``````*Mini> natInd ["X","Y"] [0,1]
P(zero,zero).
! [Y3 : Nat] : (P(zero,Y3) => P(zero,succ(Y3))).
! [X1 : Nat] : (P(X1,zero) => P(succ(X1),zero)).
! [X1 : Nat,Y3 : Nat] :
(P(X1,Y3) &
P(X1,succ(Y3)) &
P(succ(X1),Y3)
=> P(succ(X1),succ(Y3))).
``````

In the last step case, all proper subterms of `succ(X1),succ(Y3)` are used as hypotheses.

A bigger example is in `example/Example.hs` in the distribution.