A python program that finds possible solutions for a given function in propositional calculus. This program checks automatically all the combinations whether there are suitable combinations for variables that validate the new formel. That is best used in the induction step (Induktionsschritt in German) in a structural induction (Strukturelle Ind…

structurel_induction_example.py

# To decipher the result,
# 0 -> theta
# 1 -> not theta
# 2 -> psi
# 3 -> not psi

def and_op(theta, psi):
	return theta and psi

def or_op(theta, psi):
	return theta or psi

def imp_op(theta, psi):
	if theta is True and psi is False:
		return False
	else:
		return True

def biimp_op(theta, psi):
	if theta is psi:
		return True
	else:
		return False

def three_op(first, second, third):
	if (first is True and (second is False or third is False)) or (first is False and (second is third)):
		return True
	else:
		return False

def find_right_combinations(theta, psi, expected_bool_val):
	right_combinations = []
	variables = [theta, not theta, psi, not psi]
	for i in range(len(variables)):
		for j in range(len(variables)):
			for k in range(len(variables)):
				res = three_op(variables[i], variables[j], variables[k])
				if res == expected_bool_val:
					right_combinations.append([i, j, k])
	return right_combinations


def deliver_results(op):

	possible_solutions = []
	for theta in [True, False]:
		for psi in [True, False]:
			res = find_right_combinations(theta, psi, op(theta, psi))
			possible_solutions.append(res)

	first = possible_solutions[0]
	second = possible_solutions[1]
	third = possible_solutions[2]
	fourth = possible_solutions[3]

	cevap = [x for x in first if x in second]
	cevap = [x for x in cevap if x in third]
	cevap = [x for x in cevap if x in fourth]
	return cevap

if __name__ == '__main__':

	for op in [or_op, and_op, imp_op, biimp_op]:
		if op == or_op:
			print("Results for or operator: ", deliver_results(op))
		elif op == and_op:
			print("Results for and operator: ", deliver_results(op))
		elif op == imp_op:
			print("Results for implication operator: ", deliver_results(op))
		elif op == biimp_op:
			print("Results for biimplication operator: ", deliver_results(op))