%Der Operator "f" sei definiert durch: % f('$Rp','$Rq') = not '$Rp' or ('$Rq' and diamond a : ('$Rp' and not '$Rq')) or not diamond a : ('$Rp' and '$Rq'). %19. % not ( diamond a : box a : (( '$Rp' implies '$Rq') equivalent f('$Rp', f('$Rp', '$Rq')))). not ( diamond a : box a : ((('$Rp' implies '$Rq') implies (not ('$Rp') or ((not ('$Rp') or ( '$Rq' and diamond a : ( '$Rp' and not '$Rq' )) or not ( diamond a : ( '$Rp' and '$Rq' ))) and diamond a : ( '$Rp' and not (not ('$Rp') or ( '$Rq' and diamond a : ( '$Rp' and not '$Rq' )) or not ( diamond a : ( '$Rp' and '$Rq' )) ))) or not ( diamond a : ( '$Rp' and (not ('$Rp') or ( '$Rq' and diamond a : ( '$Rp' and not '$Rq' )) or not ( diamond a : ( '$Rp' and '$Rq' ))))))) and ((not ('$Rp') or ((not ('$Rp') or ( '$Rq' and diamond a : ( '$Rp' and not '$Rq' )) or not ( diamond a : ( '$Rp' and '$Rq' ))) and diamond a : ( '$Rp' and not (not ('$Rp') or ( '$Rq' and diamond a : ( '$Rp' and not '$Rq' )) or not ( diamond a : ( '$Rp' and '$Rq' )) ))) or not ( diamond a : ( '$Rp' and (not ('$Rp') or ( '$Rq' and diamond a : ( '$Rp' and not '$Rq' )) or not ( diamond a : ( '$Rp' and '$Rq' )))))) implies ('$Rp' implies '$Rq')))). %diamond a : box a : ((('$Rp' implies '$Rq') implies (not ('$Rp') or ((not ('$Rp') or ( '$Rq' and diamond a : ( '$Rp' and not '$Rq' )) or not ( diamond a : ( '$Rp' and '$Rq' ))) and diamond a : ( '$Rp' and not (not ('$Rp') or ( '$Rq' and diamond a : ( '$Rp' and not '$Rq' )) or not ( diamond a : ( '$Rp' and '$Rq' )) ))) or not ( diamond a : ( '$Rp' and (not ('$Rp') or ( '$Rq' and diamond a : ( '$Rp' and not '$Rq' )) or not ( diamond a : ( '$Rp' and '$Rq' ))))))) and ((not ('$Rp') or ((not ('$Rp') or ( '$Rq' and diamond a : ( '$Rp' and not '$Rq' )) or not ( diamond a : ( '$Rp' and '$Rq' ))) and diamond a : ( '$Rp' and not (not ('$Rp') or ( '$Rq' and diamond a : ( '$Rp' and not '$Rq' )) or not ( diamond a : ( '$Rp' and '$Rq' )) ))) or not ( diamond a : ( '$Rp' and (not ('$Rp') or ( '$Rq' and diamond a : ( '$Rp' and not '$Rq' )) or not ( diamond a : ( '$Rp' and '$Rq' )))))) implies ('$Rp' implies '$Rq'))). %%% Axioms of S4: reflexivity and transitivity # modal_axiom_schema(reflexive,a). # modal_axiom_schema(transitive,a).