%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'). %18. %not ( diamond a : box a : (diamond a : '$Rp' equivalent (f(f(f('$Rp','$Rp'),'$Rp'),'$Rp') implies '$Rp'))). not(diamond a : box a : ((diamond a : '$Rp' equivalent not (not (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : '$Rp')) or ( '$Rp' and diamond a : (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : '$Rp') and not '$Rp' )) or not ( diamond a : ( not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : '$Rp')) and '$Rp' ))) or ( '$Rp' and diamond a : ( not (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : '$Rp' )) or ( '$Rp' and diamond a : (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : '$Rp') and not '$Rp' )) or not ( diamond a : ( not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : '$Rp' ) and '$Rp' )) and not '$Rp' )) or not ( diamond a : (not (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : '$Rp' )) or ( '$Rp' and diamond a : (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : '$Rp') and not '$Rp' )) or not ( diamond a : ( not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : '$Rp' ) and '$Rp' )) and '$Rp' )) )). %diamond a : box a : ((diamond a : '$Rp' implies not (not (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' ))) or ( '$Rp' and diamond a : (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' )) and not '$Rp' )) or not ( diamond a : ( not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' )) and '$Rp' ))) or ( '$Rp' and diamond a : ( not (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' ))) or ( '$Rp' and diamond a : (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' )) and not '$Rp' )) or not ( diamond a : ( not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' )) and '$Rp' )) and not '$Rp' )) or not ( diamond a : (not (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' ))) or ( '$Rp' and diamond a : (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' )) and not '$Rp' )) or not ( diamond a : ( not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' )) and '$Rp' )) and '$Rp' )) ) and ( not (not (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' ))) or ( '$Rp' and diamond a : (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' )) and not '$Rp' )) or not ( diamond a : ( not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' )) and '$Rp' ))) or ( '$Rp' and diamond a : ( not (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' ))) or ( '$Rp' and diamond a : (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' )) and not '$Rp' )) or not ( diamond a : ( not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' )) and '$Rp' )) and not '$Rp' )) or not ( diamond a : (not (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' ))) or ( '$Rp' and diamond a : (not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' )) and not '$Rp' )) or not ( diamond a : ( not ('$Rp') or ( '$Rp' and diamond a : ( '$Rp' and not '$Rp' )) or not ( diamond a : ( '$Rp' and '$Rp' )) and '$Rp' )) and '$Rp' )) implies diamond a : '$Rp' )). %%% Axioms of S4: reflexivity and transitivity # modal_axiom_schema(reflexive,a). # modal_axiom_schema(transitive,a).