|
- # 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))
- }
|