Bit Inference

Bit vectors and bit operations are proposed for efficient propositional inference. Bit arithmetic has efficient software and hardware implementations, which can be put to advantage in Boolean satisability procedures. Sets of variables are represented as bit vectors and formul? as matrices. Symbolic operations are performed by bit arithmetic. As examples of inference done in this fashion, we describe ground resolution and ground completion. "It does take a little bit of inference." ? Tony Fratto, Deputy Press Secretary, USA

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Nachum Dershowitz
• Keywords: Automated Reasoning, Boolean Satisability Procedures, CADE 2008, Deputy Press Secretary, Efficient Propositional Inference