|
|
|
@@ -0,0 +1,50 @@ |
|
|
|
# Josua Kugler, Christian Merten
|
|
|
|
|
|
|
|
library(tidyverse)
|
|
|
|
library(rlang)
|
|
|
|
|
|
|
|
variables <- LETTERS[1:7]
|
|
|
|
names(variables) <- variables
|
|
|
|
prop_ops <- exprs(`(`,`!`,`&`,`|`,`<=`,`>=`,`==`)
|
|
|
|
prop_ops_str <- sapply(prop_ops, expr_text)
|
|
|
|
ops_expr_str <- c("==", "<=", ">=", "&", "|", "!")
|
|
|
|
ops_print_str <- c("\u2194","\u2190","\u2192","\u2227","\u2228","\u00AC")
|
|
|
|
names(ops_print_str) <- ops_expr_str
|
|
|
|
|
|
|
|
flip <- function(f) function(x,y) f(y,x)
|
|
|
|
implies <- function(A, B) (!A) | B
|
|
|
|
|
|
|
|
validate_Prop <- function(e) {
|
|
|
|
stopifnot("class must be Prop" = "Prop" %in% class(e))
|
|
|
|
stopifnot("only numbers 0 and 1 allowed" = !str_detect(expr_text(e), "[2-9]"))
|
|
|
|
stopifnot("invalid operator or variable" = all(all.names(e) %in% c(variables, ops_expr_str, "(", ")")))
|
|
|
|
e
|
|
|
|
}
|
|
|
|
|
|
|
|
Prop <- function(x) {
|
|
|
|
e <- enexpr(x)
|
|
|
|
if (typeof(e) == "symbol") e <- expr(( (!!e) ))
|
|
|
|
validate_Prop(structure(e, class="Prop"))
|
|
|
|
}
|
|
|
|
|
|
|
|
tochar <- function(p) str_replace_all(expr_text(p), fixed(ops_print_str))
|
|
|
|
|
|
|
|
print.Prop <- function(p) {
|
|
|
|
cat(tochar(p), "\n")
|
|
|
|
invisible(p)
|
|
|
|
}
|
|
|
|
|
|
|
|
interprete <- function(prop, vars, append=FALSE) {
|
|
|
|
res <- as.logical(eval_tidy(prop, c(as.list(vars),
|
|
|
|
`>=` = implies,
|
|
|
|
`<=` = flip(implies))))
|
|
|
|
var <- tochar(prop)
|
|
|
|
if(append) add_column(vars, (!!sym(var)) := res)
|
|
|
|
else res
|
|
|
|
}
|
|
|
|
|
|
|
|
combinations <- do.call(expand.grid, lapply(variables, function(v) c(0,1)))
|
|
|
|
|
|
|
|
is_tautology <- function(prop) {
|
|
|
|
all(interprete(prop, combinations))
|
|
|
|
}
|