TouIST：基于Java的逻辑语言IDE，集成SAT/SMT/QBF求解器

资源摘要信息:"TouIST是一个集成开发环境（IDE）以及一种逻辑语言，它支持使用SAT、SMT和QBF求解器进行逻辑编程和问题求解。SAT（布尔可满足性问题）求解器用于解决命题逻辑的可满足性问题，SMT（可满足性模理论）求解器用于解决带有附加理论（如整数算术、实数等）的逻辑公式，QBF（量词布尔公式）求解器则用于解决包含量词的逻辑公式。 在2018年7月4日的信息中提到了TouIST.jar在macOS上的兼容性问题，建议使用Java 8进行运行。同时介绍了如何通过Gitpod在线环境对TouIST进行开发和测试。 TouIST的安装提供了基于Java的图形界面版本，适用于多种操作系统，包括Linux、Windows和macOS。它提供了两种下载选项：一个普通的jar文件适用于所有平台，另一个是针对macOS和Windows的非签名本机版本，需要注意的是在macOS Sierra系统上可能会遇到应用程序损坏的警告消息。为了解决这个问题，需要运行命令`sudo spctl --master-disable`以暂时禁用Gatekeeper安全功能。 TouIST的主要标签包括：教育、研究、OCaml、问题解决、命题逻辑、SMT、MiniSat、SMT-LIB、SAT、DIMACS、Yices以及QBF。这些关键词涵盖了TouIST的主要功能和应用场景。其中，OCaml是开发TouIST的编程语言。命题逻辑是TouIST所使用的逻辑类型。MiniSat是一个流行的SAT求解器，TouIST支持SMT-LIB标准，这是SMT求解器的交换语言。DIMACS是SAT问题的另一个标准格式，而Yices是一个高效的QBF求解器。 文件名称列表中包含了'touist-master'，这可能意味着TouIST项目的主分支或主版本。用户可以下载和使用这个版本进行开发和测试。"