class documentation

class TableauProver(Prover): (source)

View In Hierarchy

Undocumented

Static Method is_atom Undocumented
Method _attempt_proof Undocumented
Method _attempt_proof_all Undocumented
Method _attempt_proof_and Undocumented
Method _attempt_proof_app Undocumented
Method _attempt_proof_atom Undocumented
Method _attempt_proof_d_neg Undocumented
Method _attempt_proof_eq Undocumented
Method _attempt_proof_iff Undocumented
Method _attempt_proof_imp Undocumented
Method _attempt_proof_n_all Undocumented
Method _attempt_proof_n_and Undocumented
Method _attempt_proof_n_app Undocumented
Method _attempt_proof_n_atom Undocumented
Method _attempt_proof_n_eq Undocumented
Method _attempt_proof_n_iff Undocumented
Method _attempt_proof_n_imp Undocumented
Method _attempt_proof_n_or Undocumented
Method _attempt_proof_n_prop Undocumented
Method _attempt_proof_n_some Undocumented
Method _attempt_proof_or Undocumented
Method _attempt_proof_prop Undocumented
Method _attempt_proof_some Undocumented
Method _prove No summary
Class Variable _assume_false Undocumented

Inherited from Prover:

Method prove No summary
@staticmethod
def is_atom(e): (source)

Undocumented

def _attempt_proof(self, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_and(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_app(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_d_neg(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_eq(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_iff(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_n_all(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_n_and(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_n_app(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_n_eq(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_n_iff(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_n_imp(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_n_or(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_n_prop(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_n_some(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _attempt_proof_some(self, current, context, agenda, accessible_vars, atoms, debug): (source)

Undocumented

def _prove(self, goal=None, assumptions=None, verbose=False): (source)
Returns
tuple: (bool, str)Whether the proof was successful or not, along with the proof
_assume_false: bool = (source)

Undocumented