Starting points for the Knights/Knaves tautology checker...

Possible helper rules:

This problem does not require a lot of code, but it does require some careful thinking about

• how to check whether an expression Expr contains a literal integer representing a logical variable
• how to determine whether an expression, even containing only leaves of t and f, is a tautology or unsatisfiable or neither
• how to substitute t or f into such an expression, yielding a new expression -- there are a couple examples of this above
• how to avoid having Prolog head off infinitely searching for bindings that will not be helpful

• noVars( Expr ) true if Expr has no logical variables, i.e., literal integers
  
  Here is the code we wrote in class, which you may want to adapt:

       noVars( t ).
       noVars( f ).
       noVars( [_, L, R] ) :- noVars( L ), noVars( R ).
       

  Note that you'll need another rule in order to handle not, as well.
  
  
• getVar( Expr, N ) true if N is an integer representing a variable that is currently contained in Expr. Here is a slight variant (that adds speed/efficiency!!) to the code we wrote in class:

       getVar( N, N ) :- number( N ).
       getVar( [_, L, R], N ) :- getVar( L, N ); (noVars(L), getVar( R, N )). 
       

  Note that you'll need another rule here to handle the unary logical expressions that begin with not.
  
  Note, too, that the second rule above only descends the second branch if there are no variables in the first branch! This will make the expansion much more succinct and, thus, faster and memory-efficient. Be sure to use this (the code may not complete in the time/memory available otherwise!)
  
  That said, it's worth mentioning that the above code for getVar will not bind to more than one variable in a single invocation. For example,

       ?- getVar([ifthen, 1, 2], X).
       X = 1 ;
       No
       

  Although this may seem like a problem, once you substitute a truth value for 1, the next call to getVar will happily return the 2. And, did we mention it's much faster?
  
  
• You may want to consider the next few possibilities en route to completing the overall id predicate:
  
  
• subst( N, TorF, OldExpr, NewExpr ) should be true if N is an integer representing a variable that is currently contained in OldExpr, and TorF is t or f, and NewExpr is identical to OldExpr, except that all instances of N have been replaced with the literal value of TorF.
  
  Keep in mind that you'll need subst to work even when OldExpr contains no occurrences of N, perhaps because there are no variables (integers) or perhaps because it is an integer - just not the same as N! Thus, you'll not only need a couple of recursive cases, but also a number of different base cases for subst:
  1. when OldExpr is the same as N
  2. when OldExpr has no variables
  3. when OldExpr is a number, but a number that is different from N
  
  Here are two examples of how subst might work:

       subst( 1, t, [and, [not, 1], 1], NewExpr ).
       NewExpr = [and, [not, t], t]
  
       subst( 1, t, [and, [not, 1], 2], NewExpr ).
       NewExpr = [and, [not, t], 2]
       

• eval( Expr, TorF ) would be used only when Expr has no variables -- in fact, you could avoid the explicit noVars check, if this predicate were only called appropriately by taut and/or unsat. Note that any no-variable expression must be either true t or false f.

  Then, eval( Expr, t ) would indicate that the no-variable expression Expr evaluates to true. Similarly, eval( Expr, f ) would indicate that Expr evaluates to false. Recursion is important here -- in fact, mutual recursion between the t and f cases. However, be sure that each recursive or mutually-recursive call gets closer to one of the base cases -- otherwise, it could run forever!

  If you'd like to use this, here is an example rule that may help get you started:

   
  eval( [not, SubExpr], t ) :- eval( SubExpr, f ).
  

• taut( Expr ) should be true if Expr is a tautology It's possible to write this so that taut checks for noVars and then evaluates the no-variable expression itself, or it can use eval, as noted above, for that no-variable evaluation.
  
  
• unsat( Expr ) should be true if Expr is unsatisfiable Again, you can check for noVars in many different unsat cases and handle the evaluation of no-variable expressions here -- or, you could use eval.

Checking if something is a number...

In addition, keep in mind that you can use number(N), a predicate built-in to Prolog that makes sure N is bound to a number.